On reachability in succinct and parameterised one-counter automata
Christoph Haase (Oxford University Computing Laboratory)
Info
|
Date |
4th March 2009 (week 7, Hilary Term 2009) |
|
Time |
11:30 |
|
Place |
Room 441, Oxford University Computing Laboratory |
Abstract
One-counter automata are a fundamental and widely-studied class of infinite-state systems. In this talk, 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. We 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.
Joint work with Stephan Kreutzer, Joel Ouaknine and James Worrell.
Further info
|
Related series |