@inproceedings{HKOW-09concur,
  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.",
  author = "Christoph Haase and Stephan Kreutzer and Joel Ouaknine and James Worrell",
  booktitle = "Proceedings of the 20th International Conference on Concurrency Theory (CONCUR09)",
  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",
  title = "Reachability in Succinct and Parametric One-Counter Automata",
  volume = "5710",
  year = "2009",
}