×

zbMATH — the first resource for mathematics

On the expressiveness of internal mobility in name-passing calculi. (English) Zbl 0915.68059
Summary: We consider \(\pi\)I, a fragment of the \(\pi\)-calculus where only exchange of private names among processes is permitted (internal mobility). The calculus \(\pi\)I enjoys a simpler mathematical treatment, very close to that of CCS. In particular, \(\pi\)I avoids the concept of substitution. We provide an encoding from the asynchronous \(\pi\)-calculus to \(\pi\)I and then prove that two processes are barbed-equivalent in \(\pi\)-calculus if and only if their translations in \(\pi\)I cannot be distinguished, under barbed bisimilarity, by any translated static context. The result shows that, in name-passing calculi, internal mobility is the essential ingredient as far as expressiveness is concerned.

MSC:
68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] R. Amadio, An asynchronous model of locality, failure and process mobility; available at http://protis. univ-mrs.fr/amadio/locfaIII.
[2] Amadio, R.; Castellani, I.; Sangiorgi, D.; Amadio, R.; Castellani, I.; Sangiorgi, D., On bisimulations for the asynchronous π-calculus, (), Extended abstract in · Zbl 0915.68009
[3] Arun-Kumar; Hennessy, M., An efficiency preorder for processes, Acta inform., 29, 737-760, (1992) · Zbl 0790.68039
[4] Boreale, M.; Sangiorgi, D.; Boreale, M.; Sangiorgi, D., A fully abstract semantics for causality in the π-calculus, (), An extract appeared in · Zbl 0908.68103
[5] Boreale, M.; Sangiorgi, D., Some congruence properties for π-calculus bisimilarities, (), Theoret. Comput. Sci., to appear. · Zbl 0902.68117
[6] Boudol, G., Asynchrony and the π-calculus (note), ()
[7] De Nicola, R.; Hennessy, M., Testing equivalence for processes, Theoret. comput. sci., 34, 83-133, (1984) · Zbl 0985.68518
[8] Ferrari, G.; Montanari, U.; Quaglia, P., A π-calculus with explicit substitutions, Theoret. comput. sci., 168, 2, 53-103, (1996) · Zbl 0874.68197
[9] C. Fournet, G. Gonthier, The reflexive chemical abstract machine and the join-calculus, in: Proc. 23rd Symp. on Principles of Programming Languages (PO-PL’96). · Zbl 1065.68071
[10] Hansen, M.; Kleist, J.; Hüttel, H., Bisimulations for asynchronous mobile processes, ()
[11] Honda, K., Two bisimilarities for the ν-calculus, ()
[12] Milner, R., The polyadic π-calculus: a tutorial, ()
[13] Milner, R., Functions as processes, Math. struct. comput. sci., 2, 2, 119-141, (1992) · Zbl 0773.03012
[14] Milner, R.; Parrow, J.; Walker, D.; Milner, R.; Parrow, J.; Walker, D., A calculus of mobile processes, Inform. comput., Inform. comput., 100, 42-78, (1992), Parts I and II
[15] Nestmann, U.; Pierce, B.C., Decoding choiche encodings, (), 179-194
[16] Parrow, J.; Sangiorgi, D., Algebraic theories for name-passing calculi, Inform. comput., 120, 2, 174-197, (1995) · Zbl 0836.03020
[17] Pierce, B.; Sangiorgi, D., Typing and subtyping for mobile processes, Math. struct. comput. sci., 11, (1995) · Zbl 0861.68030
[18] Sangiorgi, D., Expressing mobility in process algebras: first-order and higher-order paradigms, () · Zbl 0956.68081
[19] Sangiorgi, D.; Sangiorgi, D., Locality and non-interleaving semantics in calculi for mobile processes, (), An extract appeared in · Zbl 0874.68115
[20] Sangiorgi, D., Lazy functions and mobile processes, () · Zbl 0956.68081
[21] Sangiorgi, D., A theory of bisimulation for the π-calculus, Acta inform., 33, 69-97, (1996) · Zbl 0835.68072
[22] Sangiorgi, D., Π-calculus, internal mobility, and agent-passing calculi, Theoret. comput. sci., 167, 2, 235-274, (1996) · Zbl 0874.68103
[23] Sangiorgi, D.; Milner, R., The problem of “weak bisimulation up-to”,, (), 32-46
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.