Pushdown timed automata: a binary reachability characterization and safety verification

We consider pushdown timed automata (PTAs) that are timed automata (with dense clocks) augmented with a pushdown stack. A configuration of a PTA includes a state, dense clock values and a stack word. By using the pattern technique, we give a decidable characterization of the binary reachability (i.e...

Full description

Saved in:
Bibliographic Details
Published in:Theoretical computer science 2003-06, Vol.302 (1), p.93-121
Main Author: Dang, Zhe
Format: Article
Language:English
Subjects:
Algebra
Applied sciences
Automata. Abstract machines. Turing machines
Binary reachability
Computer science
control theory
systems
Exact sciences and technology
General logic
Logic and foundations
Mathematical logic, foundations, set theory
Mathematics
Model-checking
Number theory
Presburger
Pushdown timed automata
Real-time systems
Sciences and techniques of general use
Theoretical computing
Timed automata
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:We consider pushdown timed automata (PTAs) that are timed automata (with dense clocks) augmented with a pushdown stack. A configuration of a PTA includes a state, dense clock values and a stack word. By using the pattern technique, we give a decidable characterization of the binary reachability (i.e., the set of all pairs of configurations such that one can reach the other) of a PTA. Since a timed automaton can be treated as a PTA without the pushdown stack, we can show that the binary reachability of a timed automaton is definable in the additive theory of reals and integers. The results can be used to verify a class of properties containing linear relations over both dense variables and unbounded discrete variables. The properties previously could not be verified using the classic region technique nor expressed by timed temporal logics for timed automata and CTL ∗ for pushdown systems. The results are also extended to other generalizations of timed automata.
ISSN:0304-3975
1879-2294
DOI:10.1016/S0304-3975(02)00743-0