Actions speak louder than words: Proving bisimilarity for context-free processes. (English) Zbl 0904.68129

Summary: 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.


68Q42 Grammars and rewriting systems
68Q05 Models of computation (Turing machines, etc.) (MSC2010)
68Q45 Formal languages and automata
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
03B25 Decidability of theories and sets of sentences
Full Text: DOI Link