## Model checking succinct and parametric one-counter automata

*Stefan Göller*, *Christoph Haase*,
*Joël
Ouaknine*, and *James Worrell*
We investigate the decidability and complexity of various model
checking problems over one-counter automata. More specifically, we
consider succinct one-counter automata, in which additive updates are
encoded in binary, as well as parametric one-counter automata, in
which additive updates may be given as unspecified parameters. We
fully determine the complexity of model checking these automata
against CTL, LTL, and modal mu-calculus specifications.

*Proceedings of ICALP 10*, LNCS 6199, 2010. 12 pages.

PDF
© 2010
Springer-Verlag.

Imprint / Data Protection