Bisimulation equivalence is decidable for all context-free processes

  • Søren Christensen
  • Hans Hüttel
  • Colin Stirling
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 630)


We have shown that bisimulation equivalence is decidable for BPA. As the proof involves two semi-decision procedures it is not obvious how to determine the complexity of solving this problem. Moreover it does not provide us with an intuitive technique for deciding bisimilarity as does the tableau method in [14, 13] which also has the advantage of providing us with a way of extracting a complete axiomatization for normed BPA processes. A similar result for full BPA would be a proper extension of Milner's axiom system for regular processes [16].

More generally this work addresses the area of infinite-state processes. Besides deciding equivalences there is also the question of model checking: a recent result

Of more interest to concurrency theory are process languages with parallel combinators. Although bisimulation equivalence is undecidable for ACP, CCS, and CSP it is unclear if this must be true of all parallel models with full Turing power (especially those that lack abstraction mechanisms). Moreover there may be finer useful equivalences which permit general decidability results: for instance in [8] it is shown that distributed bisimulation equivalence is decidable for a recursive fragment of CCS with parallel.


Model Check Transition Graph Sequential Composition Behavioural Equivalence Complete Axiomatization 
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. [1]
    J.C.M. Baeten, J.A. Bergstra, and J.W. Klop. Decidability of bisimulation equivalence for processes generating context-free languages. Technical Report CS-R8632, CWI, September 1987.Google Scholar
  2. [2]
    J.A. Bergstra and J.W. Klop. Process algebra for synchronous communication. Information and Control, 60:109–137, 1984.zbMATHMathSciNetCrossRefGoogle Scholar
  3. [3]
    J.A. Bergstra and J.W. Klop. Process theory based on bisimulation semantics. In J.W. de Bakker, W.P de Roever, and G. Rozenberg, editors, LNCS 354, pages 50–122. Springer-Verlag, 1988.Google Scholar
  4. [4]
    O. Burkart and B. Steffen. Model checking for context-free processes. In these proceedings.Google Scholar
  5. [5]
    D. Caucal. Décidabilité de l'egalité des langages algébriques infinitaires simples. In Proceedings of STACS 86, LNCS 210, pages 37–48. Springer-Verlag, 1986.Google Scholar
  6. [6]
    D. Caucal. Graphes canoniques de graphes algébriques. Rapport de Recherche 872, INRIA, Juillet 1988.Google Scholar
  7. [7]
    D. Caucal. Graphes canoniques de graphes algébriques. Informatique théorique et Applications (RAIRO), 24(4):339–352, 1990.zbMATHMathSciNetGoogle Scholar
  8. [8]
    S. Christensen. Distributed bisimularity is decidable for a class of infinite statespace systems. In these proceedings.Google Scholar
  9. [9]
    J. F. Groote. A short proof of the decidability of bisimulation for normed BPA-processes. Tech. Report Utrecht University 1992.Google Scholar
  10. [10]
    J.F. Groote and H. Hüttel. Undecidable equivalences for basic process algebra. Technical Report ECS-LFCS-91-169, Department of Computer Science, University of Edinburgh, August 1991.Google Scholar
  11. [11]
    C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1988.Google Scholar
  12. [12]
    J. Hopcroft and J.D. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, 1979.Google Scholar
  13. [13]
    H. Hüttel. Decidability, Behavioural Equivalences and Infinite Transition Graphs. PhD thesis, University of Edinburgh, December 1991.Google Scholar
  14. [14]
    H. Hüttel and C. Stirling. Actions speak louder than words: Proving bisimilarity for context-free processes. In Proceedings of 6th Annual Symposium on Logic in Computer Science (LICS 91), pages 376–386. IEEE Computer Society Press, 1991.Google Scholar
  15. [15]
    Dung T. Huynh and Lu Tian. On deciding readiness and failure equivalences for processes. Technical Report UTDCS-31-90, University of Texas at Dallas, September 1990.Google Scholar
  16. [16]
    R. Milner. A complete inference system for a class of regular behaviours. Journal of Computer and System Sciences, 28:439–466, 1984.zbMATHMathSciNetCrossRefGoogle Scholar
  17. [17]
    R. Milner. Communication and Concurrency. Prentice-Hall International, 1989.Google Scholar
  18. [18]
    D. Muller and P. Schupp. The theory of ends, pushdown automata, and second-order logic. Theoretical Computer Science, 37:51–75, 1985.zbMATHMathSciNetCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • Søren Christensen
    • 1
  • Hans Hüttel
    • 2
  • Colin Stirling
    • 1
  1. 1.Laboratory for Foundations of Computer ScienceUniversity of EdinburghEdinburghScotland
  2. 2.Department of Mathematics and Computer ScienceAalborg University CentreAalborg ØDenmark

Personalised recommendations