Reachability in Succinct and Parametric One-Counter Automata

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.

• Type: Conference
• Year: 2009
• Where: CONCUR
• Authors: Christoph Haase, Stephan Kreutzer, Joël Ouaknine, James Worrell
• Keywords: CONCUR 2009, Distributed And Parallel Computing, One-counter Automata, Parametric One-counter Automata, Reachability Problem