## Bisimulation Equivalence is Decidable for all Context-Free
Processes

**Søren Christensen, Hans Hüttel, Colin Stirling**
*Abstract:* 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