×

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].

MSC:
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
PDF BibTeX XML Cite