Distributed bisimularity is decidable for a class of infinite state-space systems

  • Søren Christensen
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 630)


In general, the possibility of having parallelism within recursion will lead to systems with infinite state spaces. For instance, a language Ρ consisting of recursively defined processes over a signature of prefixing, non-deterministic choice and merge will contain infinite state-space systems; the solution to X = aX|b is such an example. Whether bisimulation [10] is decidable on Ρ is an open problem. However, in this paper we show that distributed bisimulation [2] is decidable on the language Ρ. The proof of decidability relies on a tableau decision method as utilised by Hüttel and Stirling in [6].


Normal Form Decision Procedure Terminal Node Equational Theory Axiom System 
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. LNCS 259, pp 93–114, 1987.MathSciNetGoogle Scholar
  2. [2]
    I. Castellani. Bisimulation for Concurrency. Ph.D. Thesis, Edinburgh University, CST-51-88, 1988.Google Scholar
  3. [3]
    D. Caucal. Graphes Canoniques de Graphes Algebriques. Report de Recherche 972, INRIA, Juillet 1988.Google Scholar
  4. [4]
    R.J. van Glabbeek. The Linear Time-Branching Time Spectrum. CONCUR90, LNCS 458, pp 278–297, 1990.Google Scholar
  5. [5]
    J.F. Groote and H. Hüttel. Undecidable Equivalences for Basic Process Algebra. University of Edinburgh, LFCS Report Series, ECS-LFCS-91-169, 1991.Google Scholar
  6. [6]
    H. Hüttel and C. Stirling. Actions Speak Louder that Words: Proving Bisimularity for Context-Free Processes. In Proceedings of 6th Annual Symposium on Logic in Computer Science (LICS 91), pp 376–386, IEEE Computer Society Press, 1991.Google Scholar
  7. [7]
    H. Hüttel. Silence is Golden: Branching Bisimularity is Decidable for Context-Free Processes. In Proceedings of the 3rd International Workshop on Computer-Aided Verification (CAV91), 1991.Google Scholar
  8. [8]
    D.T. Huynh and L. Tian. On deciding Readiness and Failure equivalences for Processes. Technical Report UTDCS-31-90, University of Texas at Dallas, 1990.Google Scholar
  9. [9]
    A. Kiehn. Distributed Bisimulations for Finite CCS, University of Sussex, Dept. of Computer Science, Report no. 7/89, 1989.Google Scholar
  10. [10]
    R. Milner. Communication and Concurrency. Prentice Hall, 1989.Google Scholar
  11. [11]
    R. Milner. A Complete Axiomatisation for Observational Congruence of Finite-State Behaviours. Journal of Information and Computation, Vol. 81, No. 2, May 1989.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • Søren Christensen
    • 1
  1. 1.Laboratory for Foundations of Computer ScienceUniversity of EdinburghEdinburghScotland

Personalised recommendations