Reachability in Succinct and Parametric One-Counter Automata

Book section

One-counter automata are a fundamental and widely-studied class of infinite-state systems. In this paper we consider one-counter automata with counter updates encoded in binary-which we refer to as the succinct encoding. It is easily seen that the reachability problem for this class of machines is in PSpace and is NP-hard. One of the main results of this paper is to show that this problem is in fact in NP, and is thus NP-complete. We also consider parametric one-counter automata, in which counter updates be integer-valued parameters. The reachability problem asks whether there are values for the parameters such that a final state can be reached from an initial state. Our second main result shows decidability of the reachability problem for parametric one-counter automata by reduction to existential Presburger arithmetic with divisibility. © 2009 Springer Berlin Heidelberg.

Authors: Haase, C; Kreutzer, S; Ouaknine, J; Worrell, J

• Publication status: Published
• Volume: 5710
• Pages: 369-383
• Publication date: 2009-01-01
• DOI: 10.1007/978-3-642-04081-8_25
• ISBN: 9783642040801