## Reachability in succinct and parametric one-counter automata

*Christoph Haase*, *Stephan Kreutzer*,
*Joël
Ouaknine*, and *James Worrell*
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 can take the form of 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.

*Proceedings of CONCUR 09*, LNCS 5710, 2009. 15 pages.

PDF
© 2009
Springer-Verlag.

Imprint / Data Protection