Title: Reachability in Succinct and Parametric One-Counter Automata
James Worrell (Oxford)
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.
This is joint work with Christoph Haase, Stephan Kreutzer and Joel
Ouaknine.