|Home||Online Resources||Table of Contents|
Journal of Logic and Computation, Volume 8, Issue 4: August 1998.
Actions speak louder than words: proving bisimilarity for context-free processes
H Hüttel1 and C Stirling2
1Department of Computer Science, Aalborg University, Frederik Bajers Vej 7E, 9220 Aalborg Ø, Denmark. E-mail: firstname.lastname@example.org, 2Laboratory for the Foundations of Computer Science, James Clerk Maxwell Building, University of Edinburgh, Edinburgh EH9 3JZ, UK. E-mail: email@example.com
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.
Key words: Bisimulation, context-free grammars, decidability, equational theories, infinite transition graphs, process calculi.