zbMATH — the first resource for mathematics

On simulation-checking with sequential systems. (English) Zbl 0987.68045
He, Jifeng (ed.) et al., Advances in computing science - ASIAN 2000. 6th Asian computing science conference, Penang, Malaysia, November 25-27, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1961, 133-148 (2000).
Summary: We present new complexity results for simulation-checking and model-checking 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 finite-state 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 infinite-state 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 \(\varphi\equiv\nu X.[z]\langle z\rangle X\) of the modal \(\mu\)-calculus. Consequently, model-checking with \(\varphi\) is EXPTIME-complete for pushdown processes and coNP-hard for processes of one-counter automata; b) model-checking with a fixed formula \(\diamondsuit[a] \diamondsuit[b]{\mathtt 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 \(\square\langle a\rangle \square\langle b\rangle{\mathtt 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.
For the entire collection see [Zbl 0953.00041].

68Q60 Specification and verification (program logics, model checking, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q45 Formal languages and automata