Dense-Timed Pushdown Automata
2012 (English)In: Proc. 27th ACM/IEEE Symposium on Logic in Computer Science, IEEE Computer Society, 2012, 35-44 p.Conference paper (Refereed)
We propose a model that captures the behavior of real-time recursive systems. To that end, we introduce dense-timed pushdown automata that extend the classical models of pushdown automata and timed automata, in the sense that the automaton operates on a finite set of real-valued clocks, and each symbol in the stack is equipped with a real-valued clock representing its "age". The model induces a transition system that is infinite in two dimensions, namely it gives rise to a stack with an unbounded number of symbols each of which with a real-valued clock. The main contribution of the paper is an EXPTIME-complete algorithm for solving the reachability problem for dense-timed pushdown automata.
Place, publisher, year, edition, pages
IEEE Computer Society, 2012. 35-44 p.
IdentifiersURN: urn:nbn:se:uu:diva-184780DOI: 10.1109/LICS.2012.15ISI: 000309059900009ISBN: 978-0-7695-4769-5OAI: oai:DiVA.org:uu-184780DiVA: diva2:567614
27th ACM/IEEE Symposium on Logic in Computer Science (LICS 2012), June 25-28, Dubrovnik, Croatia