Bisimulation equivalence is decidable for all context-free processes
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 .
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  it is shown that distributed bisimulation equivalence is decidable for a recursive fragment of CCS with parallel.
KeywordsModel Check Transition Graph Sequential Composition Behavioural Equivalence Complete Axiomatization
Unable to display preview. Download preview PDF.
- 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
- 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
- O. Burkart and B. Steffen. Model checking for context-free processes. In these proceedings.Google Scholar
- 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
- D. Caucal. Graphes canoniques de graphes algébriques. Rapport de Recherche 872, INRIA, Juillet 1988.Google Scholar
- S. Christensen. Distributed bisimularity is decidable for a class of infinite statespace systems. In these proceedings.Google Scholar
- J. F. Groote. A short proof of the decidability of bisimulation for normed BPA-processes. Tech. Report Utrecht University 1992.Google Scholar
- 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
- C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1988.Google Scholar
- J. Hopcroft and J.D. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, 1979.Google Scholar
- H. Hüttel. Decidability, Behavioural Equivalences and Infinite Transition Graphs. PhD thesis, University of Edinburgh, December 1991.Google Scholar
- 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
- 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
- R. Milner. Communication and Concurrency. Prentice-Hall International, 1989.Google Scholar