## Branching-time model checking of parametric one-counter automata

*Stefan Göller*, *Christoph Haase*,
*Joël
Ouaknine*, and *James Worrell*
We study the computational complexity of model checking EF logic and
modal logic on parametric one-counter automata (POCA). A POCA is a
one-counter automaton whose counter updates are either integer values
encoded in binary or integer-valued parameters. Given a formula and a
configuration of a POCA, the model-checking problem asks whether the
formula is true in this configuration for all possible valuations of
the parameters. We show that this problem is undecidable for EF logic
via reduction from Hilbert's tenth problem, however for modal logic we
prove PSPACE-completeness. Obtaining the PSPACE upper bound involves
analysing systems of linear Diophantine inequalities of exponential
size that admit solutions of polynomial size. Finally, we show that
model checking EF logic on POCA without parameters is PSPACE-complete.

*Proceedings of FOSSACS 12*, LNCS 7213, 2012. 15 pages.

PDF
© 2012
Springer-Verlag.

Imprint / Data Protection