Abstract
In this paper, we propose a compositional coalgebraic semantics of the π-calculus based on a novel approach for lifting calculi with structural axioms to coalgebraic models. We equip the transition system of the calculus with permutations, parallel composition and restriction operations, thus obtaining a bialgebra. No prefix operation is introduced, relying instead on a clause format defining the transitions of recursively defined processes. The unique morphism to the final bialgebra induces a bisimilarity relation which coincides with observational equivalence and which is a congruence with respect to the operations. The permutation algebra is enriched with a name extrusion operator δ à la De Brujin, that shifts any name to the successor and generates a new name in the first variable x 0. As a consequence, in the axioms and in the SOS rules there is no need to refer to the support, i.e., the set of significant names, and, thus, the model turns out to be first order.
Research supported in part by FET Global project PROFUNDIS and by MIUR project COMETA.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
A. Corradini, M. Groβe-Rhode, R. Heckel. Structured transition systems as lax coalgebras. In Proc. of CMCS’98, ENTS 11. Elsevier Science, 1998.
A. Corradini, R. Heckel, and U. Montanari. Compositional SOS and beyond: A coalgebraic view of open systems. Theoretical Computer Science 280:163–192, 2002.
R. De Simone. Higher level synchronising devices in MEIJE-SCCS. Theoretical Computer Science 37(3):245–267, 1985.
G. Ferrari, U. Montanari, and M. Pistore. Minimizing Transition Systems for Name Passing Calculi: A Co-algebraic Formulation. In Proc. of FoSSaCS’02, LNCS 2303. Springer, 2002.
G. Ferrari, U. Montanari, and P. Quaglia. A pi-calculus with Explicit Substitutions. Theoretical Computer Science 168(1):53–103, 1996.
M. Fiore and D. Turi. Semantics of name and value passing. In Proc. of LICS’01, IEEE. Computer Society Press, 2001.
M. Gabbay and A. Pitts. A new approach to abstract syntax involving binders. In Proc. of LICS’99, IEEE. Computer Society Press, 1999.
R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes (parts I and II). Information and Computation, 100(1):1–77, 1992.
U. Montanari and M. Pistore. Pi-Calculus, Structured Coalgebras and Minimal HD-Automata. In Proc. of MFCS’00, LNCS 1983. Springer, 2000.
U. Montanari and M. Pistore. Structured Coalgebras and Minimal HD-Automata for the pi-Calculus. Technical Report 0006-02, IRST-ITC, 2000. Available at the URL: http://sra.itc.it/paper.epl?id=MP00.
A. M. Pitts. Nominal Logic: A First Order Theory of Names and Binding. In Proc. of TACS’01, LNCS 2215. Springer, 2001.
M. Pistore. History Dependent Automata. Ph D. Thesis TD-5/99. Università di Pisa, Dipartimento di Informatica, 1999.A vailable at the URL: http://www.di.unipi.it/phd/tesi/tesi 1999/TD-5-99.ps.gz.
J.J.M.M. Rutten. Universal coalgebra: a theory of systems. Theoretical Computer Science 249(1):3–80, 2000.
D. Turi and G. Plotkin. Towards a mathematical operational semantics. In Proc. of LICS’97, IEEE. Computer Society Press, 1997.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Buscemi, M.G., Montanari, U. (2002). A First Order Coalgebraic Model of π-Calculus Early Observational Equivalence* . In: Brim, L., Křetínský, M., Kučera, A., Jančar, P. (eds) CONCUR 2002 — Concurrency Theory. CONCUR 2002. Lecture Notes in Computer Science, vol 2421. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45694-5_30
Download citation
DOI: https://doi.org/10.1007/3-540-45694-5_30
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-44043-7
Online ISBN: 978-3-540-45694-0
eBook Packages: Springer Book Archive