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: hans@cs.auc.dk, 2Laboratory for the Foundations of Computer Science, James Clerk Maxwell Building, University of Edinburgh, Edinburgh EH9 3JZ, UK. E-mail: cps@dcs.ed.ac.uk

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.

Pages 485-509


This page is run by Oxford University Press, Great Clarendon Street, Oxford OX2 6DP, UK
as part of the OUP Journals World Wide Web service.
Comments and feedback: www-admin@oup.co.uk
URL: http://www.oup.co.uk/logcom/hdb/Volume_08/Issue_04/080485.sgm.abs.html
Last modification: 11 September 1998.
Copyright© Oxford University Press, 1998.