Hüttel, Hans; Stirling, Colin Actions speak louder than words: Proving bisimilarity for context-free processes. (English) Zbl 0904.68129 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. Cited in 10 Documents 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 PDF BibTeX XML Cite \textit{H. Hüttel} and \textit{C. Stirling}, J. Log. Comput. 8, No. 4, 485--509 (1998; Zbl 0904.68129) Full Text: DOI Link OpenURL