On Simulation-Checking with Sequential Systems

Abstract

We present new complexity results for simulation-checking and modelchecking with infinite-state systems generated by pushdown automata and their proper subclasses of one-counter automata and one-counter nets (one-counter nets are ‘weak’ one-counter automata computationally equivalent to Petri nets with at most one unbounded place). As for simulation-checking, we show the following: a) simulation equivalence between pushdown processes and finite-state processes is EXPTIME-complete; b) simulation equivalence between processes of one-counter automata and finitestate processes is coNP-hard; c) simulation equivalence between processes of one-counter nets and finite-state processes is in P (to the best of our knowledge, it is the first (and rather tight) polynomiality result for simulation with infinitestate processes). As for model-checking, we prove that a) the problem of simulation-checking between processes of pushdown automata (or one-counter automata, or one-counter nets) and finite-state processes are polynomially reducible to the model-checking problem with a fixed formula ϕ ≡ νX.[z]〈z〉of the modal μ-calculus. Consequently, model-checking with ϕ. is EXPTIME-complete for pushdown processes and coNP-hard for processes of one-counter automata; b) model-checking with a fixed formula ◊[a]◊[b]ff of the logic EF (a simple fragment of CTL) is NP-hard for processes of OC nets, and model-checking with another fixed formula □〈〉□〈〉tt of EF is coNP-hard. Consequently, model-checking with any temporal logic which can express these simple formulae is computationally hard even for the (very simple) sequential processes of OC-nets.

Supported by the Grant Agency of the Czech Republic, grants No. 201/98/P046 and No. 201/00/1023.