Distributed bisimularity is decidable for a class of infinite state-space systems
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  is decidable on Ρ is an open problem. However, in this paper we show that distributed bisimulation  is decidable on the language Ρ. The proof of decidability relies on a tableau decision method as utilised by Hüttel and Stirling in .
KeywordsNormal Form Decision Procedure Terminal Node Equational Theory Axiom System
Unable to display preview. Download preview PDF.
- I. Castellani. Bisimulation for Concurrency. Ph.D. Thesis, Edinburgh University, CST-51-88, 1988.Google Scholar
- D. Caucal. Graphes Canoniques de Graphes Algebriques. Report de Recherche 972, INRIA, Juillet 1988.Google Scholar
- R.J. van Glabbeek. The Linear Time-Branching Time Spectrum. CONCUR90, LNCS 458, pp 278–297, 1990.Google Scholar
- 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
- 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
- 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
- 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
- A. Kiehn. Distributed Bisimulations for Finite CCS, University of Sussex, Dept. of Computer Science, Report no. 7/89, 1989.Google Scholar
- R. Milner. Communication and Concurrency. Prentice Hall, 1989.Google Scholar
- 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