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

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