Efficient verification algorithms for one-counter processes.

*(English)*Zbl 0973.68163
Montanari, Ugo (ed.) et al., Automata, languages and programming. 27th international colloquium, ICALP 2000, Geneva, Switzerland, July 9-15, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1853, 317-328 (2000).

Summary: We study the problem of strong/weak bisimilarity between processes of one-counter automata and finite-state processes. We show that the problem of weak bisimilarity between processes of one-counter nets (which are ‘weak’ one-counter automata) and finite-state processes is DP-hard (in particular, it means that the problem is both NP and co-NP hard). The same technique is used to demonstrate co-NP-hardness of strong bisimilarity between processes of one-counter nets. Then we design an algorithm which decides weak bisimilarity between processes of one-counter automata and finite-state processes in time which is polynomial for most ‘practical’ instances, giving a characterization of all hard instances as a byproduct. Moreover, we show how to efficiently compute a rather tight bound for the time which is needed to solve a given instance. Finally, we prove that the problem of strong bisimilarity between processes of one-counter automata and finite-state processes is in P.

For the entire collection see [Zbl 0941.00034].

For the entire collection see [Zbl 0941.00034].

##### MSC:

68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |

68Q60 | Specification and verification (program logics, model checking, etc.) |

68Q17 | Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) |

68Q25 | Analysis of algorithms and problem complexity |