Abstract
In a theory of processes the names are atomic data items which can be exchanged and tested for identity, but which admit no other functions or predicates. A well-known example of a calculus for name-passing is the π-calculus, where names additionally are used as communication ports. We provide complete axiomatisations of late and early bisimulation equivalences in such calculi. Since neither of the equivalences is a congruence we also axiomatise the corresponding largest congruences. We consider a few variations of the signature of the language; among these, a calculus of deterministic processes which is reminiscent of sequential functional programs with a conditional construct. Most of our axioms have been shown to be independent. The structure of the systems reveals the symmetries of the calculi and equivalences since they differ only by a few simple axioms.
Work supported by the ESPRIT BRA project 6454 “CONFER”.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
J.A. Bergstra and J.W. Klop. Algebra of Communicating Processes with Abstraction. Theoretical Computer Science 33:77–121 (1985).
G. Berry and G. Boudol. The Chemical Abstract Machine. Theoretical Computer Science 96:217–248 (1992).
S. Bloom and R. Tindell. Varieties of “if-then-else”. SIAM J. Computing 12(4):677–707 (1983).
M. Boreale and R. DeNicola. Testing equivalence for mobile processes. In Cleaveland (Ed): Proceedings of CONCUR '92, Stony Brook, August 1992, pages 2–16, Springer Verlag LNCS 630 (1992).
J. Groote and A. Ponse. Process algebra with guards. CWI technical report CS-R9069, Amsterdam 1990. To appear in Formal Aspects of Computing.
J. Groote and A. Ponse. Proof Theory for μCRL. CWI technical report CS-R9138, Amsterdam 1991.
I. Guessarian and J. Meseguer. On the axiomatization of “if-then-else”. SIAM J. Computing 16(2):322–357 (1987).
M. Hennessy. A Model for the π-calculus. Tech. Report 91/08, Department of Computer Science, University of Sussex, 1991.
M. Hennessy. A proof system for communicating processes with value-passing. Formal Aspects of Computing 3:346–366 (1991).
M. Hennessy and A. Ingólfsdóttir. A theory of communicating processes with value-passing. Technical Report 3/89, Univ. of Sussex 1989. To appear in Information and Computation.
M. Hennessy and H. Lin. Proof systems for message-passing process algebras. In Best (Ed): Proceedings of CONCUR '93, pages 202–216, Springer Verlag LNCS 715 (1993).
M. Hennessy and H. Lin. Symbolic bisimulations. Technical Report, University of Sussex 1992.
C.A.R. Hoare. Communicating Sequential Processes. Prentice Hall, 1985.
[H+87] C.A.R. Hoare, I. Hayes, He Jifeng, C. Morgan, A. Roscoe, J. Sanders, I. Sorensen, J. Spivey and B. Sufrin. Laws of programming. Comm. of the ACM 30(8):672–686 (1987).
B. Jonsson and J. Parrow. Deciding bisimulation equivalences for a class of non-finite-state programs. In Monien, Cori (Eds): Proceedings of the 6th Annual Symposium on Theoretical Aspects of Computer Science, February 1989, pages 421–433. Springer Verlag LNCS 349, 1989. Accepted for publication in Information and Computation.
E. Manes. Guard modules. Algebra Universalis 21:103–110 (1985).
S. Mauw. PSF — A Process Specification Formalism. Ph. D. Thesis, University of Amsterdam 1991.
J. McCarthy. A basis for a mathematical theory of computation. In Braffort, Hirschberg (Eds): Computer Programming and Formal Systems, pages 33–70, North-Holland (1963).
R. Milner. A Calculus of Communicating Systems. Springer Verlag LNCS 92, 1980.
R. Milner. Communication and Concurrency. Prentice Hall, 1989.
R. Milner. Functions as Processes. J. of Mathem. Structures in Computer Science 2(2):119–141 (1992).
R. Milner, J. Parrow and D. Walker. Modal logics for mobile processes. In Baeten, Groote (Eds): Proceedings of CONCUR '91, Amsterdam, August 1991, pages 45–60, Springer Verlag LNCS 527 (1991). Also in Theoretical Computer Science 114:149–171 (1993).
R. Milner, J. Parrow and D. Walker. A Calculus of Mobile Processes, Part I and II. Information and Computation 100:1–77 (1992).
R. Milner and D. Sangiorgi. Barbed Bisimulation, In Kuich, W. Ed: Proceedings of ICALP '92, pages 685–695, Springer Verlag LNCS 623, (1992).
J. Parrow. ‘Mismatching’ and early equivalence (π-calculus note JP13). Manuscript, Swedish Institute of Computer Science 1990.
J. Parrow and D. Sangiorgi. Algebraic theories for name-passing calculi. Reserach Report ECS-LFCS-93-262, Department of Computer Science, University of Edinburgh, 1993.
D. Sangiorgi. Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms. PhD thesis CST-99-93, Department of Computer Science, University of Edinburgh, 1992.
D. Sangiorgi. A theory of bisimulation for π-calculus. In Best (Ed): Proceedings of CONCUR '93, pages 127–142, Springer Verlag LNCS 715 (1993).
R. Sethi. Conditional expressions with equality tests. J. ACM 25(4):667–674 (1978).
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Parrow, J., Sangiorgi, D. (1994). Algebraic theories for name-passing calculi. In: de Bakker, J.W., de Roever, W.P., Rozenberg, G. (eds) A Decade of Concurrency Reflections and Perspectives. REX 1993. Lecture Notes in Computer Science, vol 803. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58043-3_27
Download citation
DOI: https://doi.org/10.1007/3-540-58043-3_27
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58043-0
Online ISBN: 978-3-540-48423-3
eBook Packages: Springer Book Archive