Bisimulation Equivalence is Decidable for all Context-Free Processes
Søren Christensen, Hans Hüttel, Colin StirlingAbstract: For finite-state processes all known behavioural equivalences can be seen to be decidable. In the setting of process algebra, an example of infinite-state systems is that of the transition graphs of context-free processes, which are the processes expressible in the calculus BPA (Basic Process Algebra). These are recursively defined processes with nondeterministic choice and sequential composition. In 1987, Baeten, Bergstra and Klop showed the surprising result that bisimulation equivalence is decidable for a subclass of such processes, the so-called normed processes where termination is always possible.
In this paper we generalize this result by showing that bisimulation is decidable for all context-free processes using a technique inspired by Caucal's proof of the decidability of language equivalence for simple algebraic grammar.
LFCS report ECS-LFCS-92-218
This report is available in the following formats:
Previous | Index | Next