Model Checking Succinct and Parametric One-Counter Automata

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 µ-calculus specifications.

• Type: Conference
• Year: 2010
• Where: ICALP
• Authors: Stefan Göller, Christoph Haase, Joël Ouaknine, James Worrell
• Keywords: Additive Updates, ICALP 2010, One-counter Automata, Programming Languages, Succinct One-counter Automata