Adding Time to Pushdown Automata

Parosh Aziz Abdulla
(Uppsala University, Sweden)
Mohamed Faouzi Atig
(Uppsala University, Sweden)
Jari Stenman
(Uppsala University, Sweden)

In this tutorial, we illustrate through examples how we can combine two classical models, namely those of pushdown automata (PDA) and timed automata, in order to obtain timed pushdown automata (TPDA). Furthermore, we describe how the reachability problem for TPDAs can be reduced to the reachability problem for PDAs.

Invited Tutorial in Uli Fahrenberg, Axel Legay and Claus Thrane: Proceedings Quantities in Formal Methods (QFM 2012), Paris, France, 28 August 2012, Electronic Proceedings in Theoretical Computer Science 103, pp. 1–16.
Published: 14th December 2012.

ArXived at: https://dx.doi.org/10.4204/EPTCS.103.1 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org