More Web Proxy on the site http://driver.im/

article

Towards a unified approach to encodability and separation results for process calculi

Author:

Daniele GorlaAuthors Info & Claims

Information and Computation, Volume 208, Issue 9

Pages 1031 - 1053

https://doi.org/10.1016/j.ic.2010.05.002

Published: 01 September 2010 Publication History

Abstract

We present a unified approach to evaluate the relative expressive power of process calculi. In particular, we identify a small set of criteria (that have already been somehow presented in the literature) that an encoding should satisfy to be considered a valid means for language comparison. We argue that the combination of such criteria is a valid proposal by noting that: (i) several well-known encodings appeared in the literature satisfy them; (ii) this notion is not trivial, because some known encodings do not satisfy all the criteria we have proposed; (iii) several well-known separation results can be formulated in terms of our criteria; and (iv) some widely believed (but never formally proved) separation results can be proved by using the criteria we propose. Moreover, the criteria defined induce general proof-techniques for separation results that can be easily instantiated to cover known case-studies.

References

[1]

Amadio, R.M., Castellani, I. and Sangiorgi, D., On bisimulations for the asynchronous π-calculus. Theoretical Computer Science. v195 i2. 291-324.

[2]

Arun-Kumar, S. and Hennessy, M., An efficiency preorder for processes. Acta Informatica. v29 i8. 737-760.

[3]

M. Baldamus, J. Parrow, B. Victor, Spi-calculus translated to pi-calculus preserving may-tests, in: Proceedings of LICS, IEEE Computer Society, 2004, pp. 22--31.

[4]

M. Baldamus, J. Parrow, B. Victor, A fully abstract encoding of the π-calculus with data terms, in: Proceedings of ICALP, LNCS, vol. 3580, Springer, 2005, pp. 1202--1213.

Digital Library

[5]

Boreale, M., On the expressiveness of internal mobility in name-passing calculi. Theoretical Computer Science. v195 i2. 205-226.

[6]

G. Boudol, Asynchrony and the π-calculus (note), Rapport de Recherche 1702, INRIA Sophia-Antipolis, May 1992.

[7]

M. Bugliesi, M. Giunti, Secure implementations of typed channel abstractions, in: Proceedings of POPL, ACM, 2007, pp. 251--262.

[8]

N. Busi, M. Gabbrielli, G. Zavattaro, Replication vs. recursive definitions in channel based calculi, in: Proceedings of ICALP'03, LNCS, vol. 2719, Springer, 2003, pp. 133--144.

[9]

N. Busi, M. Gabbrielli, G. Zavattaro, Comparing recursion, replication, and iteration in process calculi, in: Proceedings of ICALP'04, LNCS, vol. 3142, Springer, 2004, pp. 307--319.

[10]

D. Cacciagrano, F. Corradini, J. Aranda, F.D. Valencia, Linearity, persistence and testing semantics in the asynchronous pi-calculus, in: Proceedings of EXPRESS'07, ENTCS, vol. 194, No. 2, 2008, pp. 59--84.

Digital Library

[11]

Cacciagrano, D., Corradini, F. and Palamidessi, C., Separation of synchronous and asynchronous communication via testing. Theoretical Computer Science. v386 i3. 218-235.

[12]

Carbone, M. and Maffeis, S., On the expressive power of polyadic synchronisation in pi-calculus. Nordic Journal of Computing. v10 i2. 70-98.

[13]

L. Cardelli, G. Ghelli, A.D. Gordon, Mobility types for mobile ambients, in: Proceedings of ICALP'99, vol. 1644, LNCS, Springer, 1999.

[14]

Cardelli, L., Ghelli, G. and Gordon, A.D., Types for the ambient calculus. Information and Computation. v177 i2. 160-194.

[15]

L. Cardelli, A.D. Gordon, Types for mobile ambients, in: Proceedings of POPL'99, ACM, 1999, pp. 79--92.

Digital Library

[16]

Cardelli, L. and Gordon, A.D., Mobile ambients. Theoretical Computer Science. v240 i1. 177-213.

[17]

de Boer, F. and Palamidessi, C., Embedding as a tool for language comparison. Information and Computation. v108 i1. 128-157.

[18]

De Nicola, R. and Hennessy, M., Testing equivalence for processes. Theoretical Computer Science. v34. 83-133.

[19]

C. Fournet, G. Gonthier, The reflexive chemical abstract machine and the join-calculus, in: Proceedings of POPL'96, ACM, 1996, pp. 372--385.

[20]

R.J. van Glabbeek, The linear time--branching time spectrum, in: Proceedings of CONCUR'90, vol. 458, LNCS, Springer, 1990, pp. 278--297.

[21]

R.J. van Glabbeek, The linear time--branching time spectrum II; the semantics of sequential systems with silent moves, in: Proceedings of CONCUR'93, vol. 715, LNCS, Springer, 1993, pp. 66--81.

[22]

D. Gorla, On the relative expressive power of ambient-based calculi, in: Proceedings of TGC'08, LNCS, vol. 5474, Springer, 2009, pp. 141--156.

Digital Library

[23]

D. Gorla, On the relative expressive power of asynchronous communication primitives, in: Proceedings of FoSSaCS'06, LNCS, vol. 3921, Springer, 2006, pp. 47--62.

Digital Library

[24]

D. Gorla, On the relative expressive power of calculi for mobility, in: Proceedings of MFPS XXV, ENTCS, vol. 249, Elsevier, 2009, pp. 269--286.

Digital Library

[25]

D. Gorla, Synchrony vs asynchrony in communication primitives, in: Proceedings of EXPRESS'06, ENTCS, vol. 175, No. 3, Elsevier, 2007, pp. 87--108.

Digital Library

[26]

Gorla, D., Comparing communication primitives via their relative expressive power. Information and Computation. v206 i8. 931-952.

[27]

D. Gorla, Towards a unified approach to encodability and separation results for process calculi, in: Proceedings of CONCUR'08, LNCS, vol. 5201, Springer, 2008, pp. 492--507.

Digital Library

[28]

B. Haagensen, S. Maffeis, I. Phillips, Matching systems for concurrent calculi, in: Proceedings of EXPRESS'07, ENTCS, vol. 194, No. 2, 2008, pp. 85--99.

[29]

Hennessy, M. and Riely, J., Resource access control in systems of mobile agents. Information and Computation. v173. 82-120.

Digital Library

[30]

M. Herlihy, Impossibility and universality results for wait-free synchronization, in: Proceedings of PODC, ACM Press, 1988, pp. 276--290.

[31]

K. Honda, M. Tokoro, An object calculus for asynchronous communication, in: Proceedings of ECOOP'91, LNCS, vol. 512, Springer, 1991, pp. 133--147.

[32]

Honda, K. and Yoshida, N., On reduction-based process semantics. Theoretical Computer Science. v152 i2. 437-486.

[33]

C. Laneve, B. Victor, Solos in concert, in: Proceedings of ICALP'99, LNCS, vol. 1644, Springer, 1999, pp. 513--523.

[34]

Levi, F., A typed encoding of boxed into safe ambients. Acta Informatica. v42 i6. 429-500.

[35]

Merro, M. and Zappa Nardelli, F., Behavioral theory for mobile ambients. Journal of the ACM. v52 i6. 961-1023.

[36]

M. Merro, D. Sangiorgi, On asynchrony in name-passing calculi, in: Proceedings of ICALP'98, LNCS, vol. 1443, Springer, 1998, pp. 856--867.

[37]

Milner, R., Communication and Concurrency. 1989. Prentice Hall.

[38]

Milner, R., Functions as processes. Mathematical Structures in Computer Science. v2 i2. 119-141.

[39]

R. Milner, The polyadic π-calculus: a tutorial, in: Logic and Algebra of Specification, Series F. NATO ASI, vol. 94, Springer, 1993.

[40]

Milner, R., Parrow, J. and Walker, D., A calculus of mobile processes, part I/II. Information and Computation. v100. 1-77.

Digital Library

[41]

R. Milner, D. Sangiorgi, Barbed bisimulation, in: Proceedings of ICALP'92, LNCS, vol. 623, Springer, 1992, pp. 685--695.

[42]

Nestmann, U., What is a 'good' encoding of guarded choice?. Information and Computation. v156. 287-319.

Digital Library

[43]

U. Nestmann, Welcome to the jungle: a subjective guide to mobile process calculi, in: Proceedings of CONCUR'06, LNCS, vol. 4137, Springer, 2006, pp. 52--63.

Digital Library

[44]

Nestmann, U. and Pierce, B.C., Decoding choice encodings. Information and Computation. v163. 1-59.

Digital Library

[45]

Palamidessi, C., Comparing the expressive power of the synchronous and the asynchronous π-calculi. Mathematical Structures in Computer Science. v13 i5. 685-719.

[46]

C. Palamidessi, V.A. Saraswat, F.D. Valencia, B. Victor, On the expressiveness of linearity vs persistence in the asychronous pi-calculus, in: Proceedings of LICS, IEEE Computer Society, 2006, pp. 59--68.

[47]

Palamidessi, C. and Valencia, F., Recursion vs replication in process calculi: expressiveness. Bulletin of the EATCS. v87. 105-125.

[48]

J. Parrow, Trios in concert, in: Proof, Language and Interaction: Essays in Honour of Robin Milner, Foundations of Computing, MIT Press, 2000, pp. 621--637.

[49]

J. Parrow, Expressiveness of process algebras, in: Emerging Trends in Concurrency, ENTCS, vol. 209, 2008, pp. 173--186.

[50]

Phillips, I. and Vigliotti, M., Electoral systems in ambient calculi. Information and Computation. v206 i1. 34-72.

[51]

Phillips, I. and Vigliotti, M., Leader election in rings of ambient processes. Theoretical Computer Science. v356 i3. 468-494.

[52]

Plotkin, G.D., A structural approach to operational semantics. Journal of Logic and Algebraic Programming. v60--61. 17-139.

[53]

P. Quaglia, D. Walker, On synchronous and asynchronous mobile processes, in: Proceedings of FoSSaCS 2000, LNCS, vol. 1784, Springer, 2000, pp. 283--296.

[54]

Quaglia, P. and Walker, D., Types and full abstraction for polyadic pi-calculus. Information and Computation. v200. 215-246.

Digital Library

[55]

J. Rathke, V. Sassone, P. Sobocinski, Semantic barbs and biorthogonality, in: Proceedings of FoSSaCS, LNCS, vol. 4423, Springer, 2007, pp. 302--316.

[56]

Sangiorgi, D., Bisimulation in higher-order process calculi. Information and Computation. v131. 141-178.

Digital Library

[57]

Sangiorgi, D. and Walker, D., The π-Calculus: A Theory of Mobile Processes. 2001. Cambridge University Press.

[58]

Vasconcelos, V., Processes, functions, and datatypes. Theory and Practice of Object Systems. v5 i2. 97-110.

[59]

N. Yoshida, Graph types for monadic mobile processes, in: Proceedings of FSTTCS'96, LNCS, vol. 1180, Springer, 1996, pp. 371--386.

Cited By

Peters KYoshida NSobocinski PLago UEsparza J(2024)Separation and Encodability in Mixed Choice Multiparty SessionsProceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3661814.3662085(1-15)Online publication date: 8-Jul-2024
https://dl.acm.org/doi/10.1145/3661814.3662085
Hüttel HLybech SBendixen ABojesen B(2024)A generic type system for higher-order Ψ-calculiInformation and Computation10.1016/j.ic.2024.105190300:COnline publication date: 1-Oct-2024
https://dl.acm.org/doi/10.1016/j.ic.2024.105190
Peters KYoshida N(2024)Mixed choice in session typesInformation and Computation10.1016/j.ic.2024.105164298:COnline publication date: 1-Jun-2024
https://dl.acm.org/doi/10.1016/j.ic.2024.105164
Show More Cited By

Towards a unified approach to encodability and separation results for process calculi
1. Theory of computation
  1. Semantics and reasoning

Recommendations

On the Expressiveness and Decidability of Higher-Order Process Calculi
LICS '08: Proceedings of the 2008 23rd Annual IEEE Symposium on Logic in Computer Science

In higher-order process calculi the values exchanged in communications may contain processes. A core calculus of higher-order concurrency is studied; it has only the operators necessary to express higher-order communications: input prefix, process ...
On the expressiveness and decidability of higher-order process calculi

In higher-order process calculi, the values exchanged in communications may contain processes. A core calculus of higher-order concurrency is studied; it has only the operators necessary to express higher-order communications: input prefix, process ...
Psi-Calculi in Isabelle

This paper presents a mechanisation of psi-calculi, a parametric framework for modelling various dialects of process calculi including (but not limited to) the pi-calculus, the applied pi-calculus, and the spi calculus. psi-calculi are significantly ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Information and Computation

Information and Computation Volume 208, Issue 9

September, 2010

95 pages

ISSN:0890-5401

Issue’s Table of Contents

Copyright © Elsevier Inc. © 2010.

Publisher

Academic Press, Inc.

United States

Publication History

Published: 01 September 2010

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

31
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 05 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Peters KYoshida NSobocinski PLago UEsparza J(2024)Separation and Encodability in Mixed Choice Multiparty SessionsProceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3661814.3662085(1-15)Online publication date: 8-Jul-2024
https://dl.acm.org/doi/10.1145/3661814.3662085
Hüttel HLybech SBendixen ABojesen B(2024)A generic type system for higher-order Ψ-calculiInformation and Computation10.1016/j.ic.2024.105190300:COnline publication date: 1-Oct-2024
https://dl.acm.org/doi/10.1016/j.ic.2024.105190
Peters KYoshida N(2024)Mixed choice in session typesInformation and Computation10.1016/j.ic.2024.105164298:COnline publication date: 1-Jun-2024
https://dl.acm.org/doi/10.1016/j.ic.2024.105164
Lybech S(2024)The reflective higher-order calculusInformation and Computation10.1016/j.ic.2024.105138297:COnline publication date: 1-Mar-2024
https://dl.acm.org/doi/10.1016/j.ic.2024.105138
Carbone MCastro-Perez DFerreira FGheri LJacobsen FMomigliano APadovani LScalas ATirore DVassor MYoshida NZackon D(2024)The Concurrent Calculi Formalisation BenchmarkCoordination Models and Languages10.1007/978-3-031-62697-5_9(149-158)Online publication date: 17-Jun-2024
https://dl.acm.org/doi/10.1007/978-3-031-62697-5_9
van Glabbeek R(2023)Comparing the Expressiveness of the π-calculus and CCSACM Transactions on Computational Logic10.1145/361101325:1(1-58)Online publication date: 18-Nov-2023
https://dl.acm.org/doi/10.1145/3611013
van den Heuvel BPaulus JNantes-Sobrinho DPérez J(2023)Typed Non-determinism in Functional and Concurrent CalculiProgramming Languages and Systems10.1007/978-981-99-8311-7_6(112-132)Online publication date: 26-Nov-2023
https://dl.acm.org/doi/10.1007/978-981-99-8311-7_6
Frumin DD’Osualdo Evan den Heuvel BPérez J(2022)A bunch of sessions: a propositions-as-sessions interpretation of bunched implications in channel-based concurrencyProceedings of the ACM on Programming Languages10.1145/35633186:OOPSLA2(841-869)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563318
Peters KNestmann USchmitt A(2022)On distributabilityTheoretical Computer Science10.1016/j.tcs.2022.03.028913:C(151-173)Online publication date: 20-Apr-2022
https://dl.acm.org/doi/10.1016/j.tcs.2022.03.028
Casal FMordido AVasconcelos V(2022)Mixed sessionsTheoretical Computer Science10.1016/j.tcs.2021.08.005897:C(23-48)Online publication date: 2-Jan-2022
https://dl.acm.org/doi/10.1016/j.tcs.2021.08.005
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Issue’s Table of Contents