Technical Reports

The report FIMU-RS-2000-03

Efficient Verification Algorithms for One-Counter Processes

by Antonín Kuèera, This is a full version of the paper presented at ICALP 2000. March 2000, 24 pages.

FIMU-RS-2000-03. Available as Postscript, PDF.

Abstract:

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.