2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (2017)
June 20, 2017 to June 23, 2017
Lorenzo Clemente , Faculty of Mathematics, Informatics and Mechanics, University of Warsaw, Poland
Slawomir Lasota , Faculty of Mathematics, Informatics and Mechanics, University of Warsaw, Poland
Ranko Lazic , DIMAP, Department of Computer Science, University of Warwick, UK
Filip Mazowiecki , DIMAP, Department of Computer Science, University of Warwick, UK
We prove that non-emptiness of timed register pushdown automata is decidable in doubly exponential time. This is a very expressive class of automata, whose transitions may involve state and top-of-stack clocks with unbounded differences. It strictly subsumes pushdown timed automata of Bouajjani et al., dense-timed pushdown automata of Abdulla et al., and orbit-finite timed register pushdown automata of Clemente and Lasota. Along the way, we prove two further decidability results of independent interest: for non-emptiness of least solutions to systems of equations over sets of integers with addition, union and intersections with ℕ and −ℕ, and for reachability in one-dimensional branching vector addition systems with states and subtraction, both in exponential time.
Registers, Automata, Clocks, Mathematical model, Orbits, Upper bound, Handheld computers
L. Clemente, S. Lasota, R. Lazic and F. Mazowiecki, "Timed pushdown automata and branching vector addition systems," 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Reykjavik, Iceland, 2017, pp. 1-12.