×

A fully abstract denotational semantics for the \(\pi\)-calculus. (English) Zbl 1014.68105

Summary: This paper describes the construction of two set-theoretic denotational models for the \(\pi\)-calculus. The models are obtained as initial solutions to domain equations in a functor category. By associating with each syntactic construct of the \(\pi\)-calculus a natural transformation over these models we obtain two interpretations for the language. We also show that these models are fully abstract with respect to natural behavioural preorders over terms in the language. By this we mean that two terms are related behaviourally if and only if their interpretations in the model are related. The behavioural preorders are the standard versions of may and must testing adapted to the \(\pi\)-calculus.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q55 Semantics in the theory of computing

Software:

Facile
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Abramsky, S., A domain equation for bisimulation, Inform. and comput., 92, 161-218, (1991) · Zbl 0718.68057
[2] Abramsky, S.; Ong, C., Full abstraction in the lazy lambda calculus, Inform. and comput., 105, 159-267, (1989) · Zbl 0779.03003
[3] Barendregt, H., The lambda calculus studies in logic, vol. 103, (1984), North-Holland Amsterdam · Zbl 0549.03012
[4] Boreale, M.; DeNicola, R., Testing for mobile processes, Inform. and comput., 120, 279-303, (1995) · Zbl 0835.68073
[5] Boudol, G., A lambda calculus for (strict) parallel functions, Inform. and comput., 108, 51-127, (1994) · Zbl 0796.03021
[6] Crole, R., Categories for types, (1993), Cambridge University Press Cambridge · Zbl 0837.68077
[7] DeNicola, R.; Hennessy, M., Testing equivalences for processes, Theoret. comput. sci., 24, 83-113, (1984) · Zbl 0985.68518
[8] Oles, F.J., Type algebras, functor categories and block structure, (), 543-573
[9] Gunter, C., Semantics of programming languages, (1992), MIT Press Cambridge, MA
[10] Hennessy, M., An algebraic theory of processes, (1988), MIT Press Cambridge, MA
[11] M. Hennessy, A Model for the \(π\) Calculus, Tech. Report 8/91, University of Sussex, 1991.
[12] Hennessy, M.; Ingolfsdottir, A., A theory of communicating processes with value-passing, Inform. and comput., 107, 2, 202-236, (1993) · Zbl 0794.68098
[13] D.J. Howe, Equality in lazy computation systems. Proc. 4th IEEE Symp. on Logic in Computer Science, 1989 pp. 198-203. · Zbl 0716.68065
[14] Milner, R., Communication and concurrency, (1989), Prentice-Hall Englewood Cliffs, NJ · Zbl 0683.68008
[15] Milner, R.; Parrow, J.; Walker, D., A calculus of mobile processes, part i, Inform. and comput., 100, 1, 1-40, (1992) · Zbl 0752.68036
[16] Milner, R.; Parrow, J.; Walker, D., A calculus of mobile processes, part ii, Inform. and comput., 100, 1, 41-77, (1992) · Zbl 0752.68037
[17] R. Milner, The polyadic \(π\)-calculus: a tutorial, Proc. Internat. Summer School on Logic and Algebra of Specification, Marktoberdorf, 1991.
[18] Moggi, E., Notions of computation and monad, Inform. and comput., 93, 55-92, (1991) · Zbl 0723.68073
[19] E. Moggi, M.P. Fiore, D. Sangiorgi, A fully-abstract model for the \(π\)-calculus Proc. LICS’96, 1996. · Zbl 1053.68066
[20] P.W. O’Hearn, R.D. Tennant, Semantics of local variables. Applications of Categories in Computer Science London Mathematical Society Lecture Note Series, Cambridge University Press, Cambridge, 1992 pp. 217-238.
[21] Parrow, J.; Sangiorgi, D., Algebraic theories for name-passing calculi, Inform. and comput., 120, 174-197, (1995) · Zbl 0836.03020
[22] A.M. Pitts, I. Stark, On the observable properties of higher order functions that dynamically create local names, or: what’s new, Proc. Mathematical Foundations of Computer Science, Springer, Berlin, 1993, pp. 122-141.
[23] D. Sangiorgi, Expressing mobility in process algebras: first-order and higher-order paradigms, Ph.D. Thesis, Edinburgh University, Scotland, 1992.
[24] D. Sangiorgi, A theory of bisimulation for the \(π\)-calculus, Proc. CONCUR’93, Lecture Notes in Computer Science, vol. 715 in 1993. · Zbl 0835.68072
[25] I. Stark, A fully-abstract domain model for the \(π\)-calculus, Proc. LICS’96, 1996.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.