Abstract: Recently Baeten, Bergstra, and Klop have proved the remarkable result that bisimulation equivalence is decidable for irredundant context-free grammars. In this paper we provide a much simpler and much more direct proof of this result using a tableau decision method involving goal-directed rules. The decision procedure yields an upper bound on the depth of a tableau. Moreover, it provides the essential part of the bisimulation relation between two processes which underlies their equivalence. A second virtue is that it provides a sound and complete equational theory for such processes.
LFCS report ECS-LFCS-91-145
This report is available in the following formats:Previous | Index | Next