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

Hüttel, Hans; Stirling, Colin

J. Log. Comput. 8, No. 4, 485-509 (1998).

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.

MSC:

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

Keywords:

bisimulation equivalence; irredundant context-free grammars; tableau decision method; goal-directed rules