2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (2017)

Reykjavik, Iceland

June 20, 2017 to June 23, 2017

ISBN: 978-1-5090-3019-4

pp: 1-12

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

ABSTRACT

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.

INDEX TERMS

Registers, Automata, Clocks, Mathematical model, Orbits, Upper bound, Handheld computers

CITATION

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.

doi:10.1109/LICS.2017.8005083

CITATIONS

SEARCH