Department of Information Technology

On the complexity of model checking 1-counter machines

  • Joint work with Anthony Widjaja To and Stefan Goeller

The complexity of model checking pushdown automata is already well established.
While reachability is polynomial, EF model checking is PSPACE-complete and EG/CTL/mu-calculus model checking is EXPTIME-complete, and the lower bounds hold even for a fixed formula, respectively.
1-counter machines can be seen as a special case of pushdown automata with only one stack symbol (plus the bottom symbol).
Recent results show that model checking 1-counter machines is easier.
Mu-calculus model checking is PSPACE-complete, while EF model checking is in P^{NP} and hard for the class P^{NP[log n]}, i.e., low in the polynomial hierarchy.
With similar techniques it can be shown that checking weak bisimulation equivalence between 1-counter machines and finite automata is also in P^{NP} and hard for P^{NP[log n]}.

Updated  2008-12-04 15:02:09 by Frédéric Haziza.