Bisimulation Equivalence is Decidable for One-Counter Processes

by Petr Jančar, Accepted for presentation at the 24th International Colloquium on Automata, Languages, and Programming (ICALP`97). May 1997, 13 pages.

FIMU-RS-97-06. Available as Postscript, PDF.

Abstract:

It is shown that bisimulation equivalence is decidable for the processes generated by (nondeterministic) pushdown automata where the pushdown behaves like a counter, in fact. Also regularity, i.e. bisimulation equivalence with some finite-state process, is shown to be decidable for the mentioned processes.