Abstract
In a previous paper the authors proved the decidability of bisimulation equivalence over two subclasses of recursive processes involving a parallel composition operator, namely the so-called normed and live processes. In this paper, we extend this result to the whole class. The decidability proof permits us further to present a complete axiomatisation for this class of basic parallel processes. This result can be viewed as a proper extension of Milner's complete axiomatisation of bisimulation equivalence on regular processes.
On leave from The School of Mathematics and Computer Science, Tel Aviv University.
Supported by ESPRIT BRA 7166: CONCUR2.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
J.C.M. Baeten, J.A. Bergstra and J.W. Klop. Decidability of bisimulation equivalence for processes generating context-free languages. In Proceedings of PARLE 87, J.W. de Bakker, A.J. Nijman, P.C. Treleaven (eds), Lecture Notes in Computer Science 259, pp93–114. Springer-Verlag, 1987.
I. Castellani. Bisimulations for Concurrency. PhD thesis CST-51-88. University of Edinburgh, 1988.
D. Caucal. Graphes canoniques des graphes algébriques. Informatique Théorique et Applications (RAIRO) 24(4), pp339–352, 1990.
S. Christensen. Distributed bisimilarity is decidable for a class of infinite-state systems. In Proceedings of CONCUR 92, W.R. Cleaveland (ed), Lecture Notes in Computer Science 630, pp148–161. Springer-Verlag, 1992.
S. Christensen. Forthcoming PhD thesis. University of Edinburgh, 1993.
S. Christensen, Y. Hirschfeld and F. Moller. Decomposability, decidability and axiomatisability for bisimulation equivalence on basic parallel processes. In Proceedings of LICS93. IEEE Computer Society Press, 1993.
S. Christensen, H. Hüttel and C. Stirling. Bisimulation equivalence is decidable for all context-free processes. In Proceedings of CONCUR 92, W.R. Cleaveland (ed), Lecture Notes in Computer Science 630, pp138–147. Springer-Verlag, 1992.
R.J. van Glabbeek. The linear time-branching time spectrum. In Proceedings of CONCUR 90, J. Baeten, J.W. Klop (eds), Lecture Notes in Computer Science 458, pp278–297. Springer-Verlag, 1990.
J.F. Groote. A short proof of the decidability of bisimulation for normed BPA processes. Information Processing Letters 42, pp167–171, 1991.
J.F. Groote and H. Hüttel. Undecidable equivalences for basic process algebra. Research report ECS-LFCS-91-169. University of Edinburgh, August 1991.
Y. Hirshfeld. Finitely generated processes, Petri nets and the equivalence problem. Unpublished notes, University of Edinburgh, May 1993.
H. Hüttel. Decidability, Behavioural Equivalences and Infinite Transition Graphs. PhD thesis CST-86-91. University of Edinburgh, December 1991.
H. Hüttel and C. Stirling. Actions speak louder than words: proving bisimilarity for context-free processes. In Proceedings of LICS 91, pp376–386. IEEE Computer Society Press, 1991.
D.T. Huynh and L. Tian. On deciding readiness and failures equivalences for processes. Research report UTDCS-31-90. University of Texas at Dallas, September 1990.
P. Jančar. Decidability questions for bisimilarity of Petri nets and some related problems. Research report ECS-LFCS-93-261. University of Edinburgh, April 1993.
D. Kozen. A completeness theorem for Kleene algebras and the algebra of regular events. In Proceedings of LICS 91, pp214–225. IEEE Computer Society Press, 1991.
Madelaine, E., Verification tools from the CONCUR project. Bulletin of the European Association of Theoretical Computer Science 47, pp110–126, June 1992.
R. Milner. A complete inference system for a class of regular behaviours. Journal of Computer and System Sciences 28, pp439–466, 1984.
R. Milner. Communication and Concurrency. Prentice-Hall, 1989.
R. Milner and F. Moller. Unique decomposition of processes. Bulletin of the European Association for Theoretical Computer Science 41, pp226–232, 1990.
F. Moller. Axioms for Concurrency. PhD thesis CST-59-89. University of Edinburgh, 1989.
A. Salomaa, Two complete axiom systems for the algebra of regular events. Journal of the Association of Computing Machinery 13, pp158–169, 1966.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Christensen, S., Hirshfeld, Y., Moller, F. (1993). Bisimulation equivalence is decidable for basic parallel processes. In: Best, E. (eds) CONCUR'93. CONCUR 1993. Lecture Notes in Computer Science, vol 715. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57208-2_11
Download citation
DOI: https://doi.org/10.1007/3-540-57208-2_11
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57208-4
Online ISBN: 978-3-540-47968-0
eBook Packages: Springer Book Archive