Reachability in Succinct and Parametric One−Counter Automata
Christoph Haase‚ Stephan Kreutzer‚ Joel Ouaknine and James Worrell
Abstract
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.
Details
| Book Title |
Proceedings of the 20th International Conference on Concurrency Theory (CONCUR'09) |
| Copyright |
Springer−Verlag |
| Editor |
M. Bravetti and G. Zavattaro |
| Location |
Bologna‚ Italy |
| Month |
September |
| Pages |
369–383 |
| Publisher |
Springer |
| Series |
Lecture Notes in Computer Science |
| Volume |
5710 |
| Year |
2009 |
Links
Related pages
|
People |