Actions Speak Louder than Words: Proving Bisimilarity for Context-Free Processes

Hans Hüttel and Colin Stirling

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