An elementary bisimulation decision procedure for arbitrary context-free processes

  • Olaf Burkart
  • Didier Caucal
  • Bernhard Steffen
Contributed Papers Concurrency
Part of the Lecture Notes in Computer Science book series (LNCS, volume 969)


We present an elementary algorithm for deciding bisimulation between arbitrary context-free processes. This improves on the state of the art algorithm of Christensen, Hüttel and Stirling consisting of two semi-decision procedures running in parallel, which prohibits any complexity estimation. The point of our algorithm is the effective construction of a finite relation characterizing all bisimulation equivalence classes, whose mere existence was exploited for the above mentioned decidability result.


Binary Relation Decision Procedure Sequential Composition Label Transition System Initial Base 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [BBK87]
    J.C.M. Baeten, J.A. Bergstra, and J.W. Klop. Decidability of Bisimulation Equivalence for Processes Generating Context-Free Languages. In PARLE '87, LNCS 259, pages 94–113. Springer, 1987. Full version appeared as: Technical Report CS-R8632, CWI, Sep. 1987.Google Scholar
  2. [BCS94]
    O. Burkart, D. Caucal, and S. Steffen. An Elementary Bisimulation Decision Procedure for Arbitrary Context-Free Processes. Technical Report AIB-94-28, RWTH Aachen, 1994.Google Scholar
  3. [BW90]
    J.C.M. Baeten and W.P. Weijland. Process Algebra, volume 18 of Cambridge Tracts in TCS. Cambridge University Press, 1990.Google Scholar
  4. [Cau89]
    D. Caucal. A Fast Algorithm to Decide on Simple Grammars Equivalence. In Int. Symposium on Optimal Algorithms, LNCS 401, pages 66–85. Springer, 1989.Google Scholar
  5. [Cau90]
    D. Caucal. Graphes Canoniques de Graphes Algébriques. RAIRO, 24(4):339–352, 1990. A preliminary, version appeared as: Rapport de Recherche 872, INRIA, July 1988.Google Scholar
  6. [CHS92]
    S. Christensen, H. Hüttel, and C. Stirling. Bisimulation Equivalence is Decidable for all Context-Free Processes. In CONCUR '92, LNCS 630, pages 138–147. Springer, 1992.Google Scholar
  7. [Gla90]
    R.J. van Glabbeek. The Linear Time — Branching Time Spectrum. In CONCUR 90, LNCS 458, pages 278–297. Springer, 1990.Google Scholar
  8. [Gro91]
    J.F. Groote. A Short Proof of the Decidability of Bisimulation for Normed BPA-Processes. Technical Report CS-R9151, CWI, Dec 1991.Google Scholar
  9. [HJM94]
    Y. Hirshfeld, M. Jerrum, and F. Moller. A Polynomial Algorithm for Deciding Bisimilarity of Normed Context-Free Processes. Technical Report ECS-LFCS-94-286, LFCS, Edinburgh, March 1994. To be presented at FOCS '94.Google Scholar
  10. [HM94]
    Y. Hirshfeld and F. Moller. A Fast Algorithm for Deciding Bisimilarity of Normed Context-Free Processes. In CONCUR '94, LNCS 836, pages 48–63, 1994.Google Scholar
  11. [Hoa85]
    C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.Google Scholar
  12. [HS91]
    H. Hüttel and C. Stirling. Actions Speak Louder than Words: Proving Bisimilarity for Context-Free Processes. In LICS '91, pages 376–386. IEEE Computer Society Press, 1991.Google Scholar
  13. [HT94]
    D.T. Huynh and L. Tian. Deciding Bisimilarity of Normed Context-Free Processes is in Deciding Bisimilarity of Normed Context-Free Processes is in σ 2p. Theoretical Computer Science, 123:183–197, 1994.CrossRefGoogle Scholar
  14. [Mil89]
    R. Milner. Communication and Concurrency. Prentice-Hall, 1989.Google Scholar
  15. [Par81]
    D. Park. Concurrency and Automata on Infinite Sequences. In 5th GI Conference, LNCS 104, pages 167–183. Springer, 1981.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Olaf Burkart
    • 1
  • Didier Caucal
    • 2
  • Bernhard Steffen
    • 3
  1. 1.Lehrstuhl für Informatik IIRWTH AachenAachenGermany
  2. 2.IRISARennesFrance
  3. 3.Fakultät für Mathematik und InformatikUniversität PassauPassauGermany

Personalised recommendations