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

Baeten, Bergstra, and Klop (and later Caucal) 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 also provides the essential part of the bisimulation relation between two processes which underlies their equivalence. We also show how to obtain a sound and complete sequent-based equational theory for such processes from the tableau system and how one can extract what Caucal calls a fundamental relation from a successful tableau. An earlier shorter version of this paper appeared at the 6th Annual Symposium on

• Type: Conference
• Year: 1991
• Where: LICS
• Authors: Hans Hüttel, Colin Stirling
• Keywords: Automated Reasoning, Bisimulation Equivalence, Irredundant Context-free Grammars, LICS 1991, Tableau Decision Method