We study decidability of verification problems for timed automata extended with unbounded discrete data structures. More detailed, we extend timed automata with a pushdown stack. In this way, we obtain a strong model that may for instance be used to model real-time programs with procedure calls. It is long known that the reachability problem for this model is decidable. The goal of this paper is to identify subclasses of timed pushdown automata for which the language inclusion problem and related problems are decidable. © 2014 Springer-Verlag.
CITATION STYLE
Quaas, K. (2014). Verification for timed automata extended with unbounded discrete data structures. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8704 LNCS, pp. 512–526). Springer Verlag. https://doi.org/10.1007/978-3-662-44584-6_35
Mendeley helps you to discover research relevant for your work.