×

Behavioural equivalences of a probabilistic pi-calculus. (English) Zbl 1270.68209

Summary: Although different kinds of probabilistic \(\pi\)-calculus have been introduced and found their place in quantitative verification and evaluation, their behavioural equivalences still lack a deep investigation. We propose a simple probabilistic extension of the \(\pi\)-calculus, \(\pi_p\), which is inspired by Herescu and Palamidessi’s probabilistic asynchronous \(\pi\)-calculus. An early semantics of our \(\pi_p\) is presented. We generalize several classic behavioural equivalences to probabilistic versions, obtaining the probabilistic (strong) barbed equivalence and probabilistic bisimulation for \(\pi_p\). Then we prove that the coincidence between the barbed equivalence and bisimilarity in the \(\pi\)-calculus is preserved in the probabilistic setting.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q87 Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Bergstra J A, Ponse A, Smolka S A, et al. Handbook of Process Algebra. Amsterdam-Lausanne-New York-Oxford-Shannon-Tokyo: Elsevier Science, 2001 · Zbl 0971.00006
[2] Milner R. A Calculus of Communicating Systems. Lect Notes Comput Sci, Vol 92. New York: Springer-Verlag, 1980 · Zbl 0452.68027
[3] Milner R. Communication and Concurrency. Englewood Cliffs, New Jersey: Prentice-Hall, 1989
[4] Bergstra J A, Klop J W. Algebra of communicating processes with abstraction. Theor Comput Sci, 1985, 37: 77–121 · Zbl 0579.68016 · doi:10.1016/0304-3975(85)90088-X
[5] Hoare C A R. Communicating sequential processes. Commun ACM, 1978, 21: 666–677 · Zbl 0383.68028 · doi:10.1145/359576.359585
[6] Hoare C A R. Communicating Sequential Processes. Englewood Cliffs, New Jersey: Prentice-Hall, 1985 · Zbl 0637.68007
[7] Milner R, Parrow J, Walker D. A calculus of mobile processes, parts I and II. Inf Comput, 1992, 100: 1–77 · Zbl 0752.68036 · doi:10.1016/0890-5401(92)90008-4
[8] Milner R. Communicating and Mobile Systems: the {\(\pi\)}-Calculus. Cambridge: Cambridge University Press, 1999 · Zbl 0942.68002
[9] De Nicola R, Hennessy M C B. Testing equivalences for processes. Theor Comput Sci, 1984, 34: 83–133 · Zbl 0985.68518 · doi:10.1016/0304-3975(84)90113-0
[10] Padget J, Bradford R. A {\(\pi\)}-calculus model of a spanish fish market: preliminary report. In: Noriega P, Sierra C, eds. Agent Mediated Electronic Commerce. Berlin/Heidelberg: Springer, 1999. 166–188
[11] Boudol G. Asynchrony and the {\(\pi\)}-calculus (note). Rapport de Recherche 1702, INRIA Sophia-Antipolis, 1992
[12] Honda K, Tokoro M. An object calculus for asynchronous communication. In: America P, ed. Proceedings of European Conference on Object-Oriented Programming, 1991. 133–147
[13] Abadi M, Gordon A D. A calculus for cryptographic protocols: the spi calculus. In: Proceedings of the 4th ACM Conference on Computer and Communications Security. New York: ACM, 1997. 36–47
[14] López N, Núñez M. An overview of probabilistic process algebras and their equivalences. In: Baier C, Haverkort B, Hermanns H, et al., eds. Validation of Stochastic Systems. Berlin/Heidelberg: Springer, 2004. 89–123 · Zbl 1203.68115
[15] Baeten J, Bergstra J, Smolka S. Axiomatizing probabilistic processes: ACP with generative probabilities. Inf Comput, 1995, 122: 234–255 · Zbl 0829.60044 · doi:10.1006/inco.1995.1135
[16] Hansson H, Jonsson B. A calculus for communicating systems with time and probabilities. In: Proceedings of the 11th Real-Time Systems Symposium, Lake Buena Vista, 1990. 278–287
[17] Seidel K. Probabilistic communicating processes. Theor Comput Sci, 1995, 152: 219–249 · Zbl 0872.68111 · doi:10.1016/0304-3975(94)00286-0
[18] Herescu O M, Palamidessi C. Probabilistic asynchronous {\(\pi\)}-calculus. In: Tiuryn J, ed. Proceedings of the 3rd International Conference on Foundations of Software Science and Computation Structures: Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000. 146–160
[19] Hermanns H, Herzog U, Katoen J-P. Process algebra for performance evaluation. Theor Comput Sci, 2002, 274: 43–87 · Zbl 0992.68149 · doi:10.1016/S0304-3975(00)00305-4
[20] Priami C. Stochastic {\(\pi\)}-calculus. Comput J, 1995, 38: 578–589 · Zbl 05478217 · doi:10.1093/comjnl/38.7.578
[21] Ying M. pi-calculus with noisy channels. Acta Inform, 2005, 41: 525–593 · Zbl 1079.68067 · doi:10.1007/s00236-005-0168-0
[22] Cao Y. Reliability of mobile processes with noisy channels. IEEE Trans Comput, 2011, doi: 10.1109/TC.2011.147, in press · Zbl 1365.94261
[23] Huang S, Cao Y, Wang H, et al. Value-passing CCS with noisy channels. Theor Comput Sci, 2012, 433: 43–59 · Zbl 1251.68157 · doi:10.1016/j.tcs.2012.03.002
[24] Cao Y. A hierarchy of behavioral equivalences in the {\(\pi\)}-calculus with noisy channels. Comput J, 2010, 53: 3–20 · doi:10.1093/comjnl/bxn006
[25] Segala R, Lynch N. Probabilistic simulations for probabilistic processes. Nord J Comput, 1995, 2: 250–273 · Zbl 0839.68067
[26] Sokolova A, De Vink E P. Probabilistic automata: system types, parallel composition and comparison. In: Baier C, Haverkort B R, Hermanns H, et al., eds. Validation of Stochastic Systems. Berlin/Heidelberg: Springer, 2004. 1–44
[27] van Glabbeek R J, Smolka S A, Steffen B, et al. Reactive, generative, and stratified models of probabilistic processes. In: Mitchell J C, ed. Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science, 1990. 130–141 · Zbl 0832.68042
[28] Giacalone A, Jou C-C, Smolka S A. Algebraic reasoning for probabilistic concurrent systems. In: Broy M, Jones C B, eds. Proceedings of Working Conference on Programming Concepts and Methods IFIP TC2, 1990. 443–458
[29] Milner R. Calculi for synchrony and asynchrony. Theor Comput Sci, 1983, 25: 267–310 · Zbl 0512.68026 · doi:10.1016/0304-3975(83)90114-7
[30] Bhargava M, Palamidessi C. Probabilistic anonymity. In: Abadi M, De Alfaro L, eds. Proceedings of the 16th International Conference on Concurrency Theory, 2005. 171–185 · Zbl 1134.68426
[31] Pradalier S, Palamidessi C. Expressiveness of probabilistic {\(\pi\)}-calculus. Electr Notes Theor Comput Sci, 2006, 164: 119–136 · doi:10.1016/j.entcs.2006.07.015
[32] Chatzikokolakis K, Palamidessi C. A framework for analyzing probabilistic protocols and its application to the partial secrets exchange. In: De Nicola R, Sangiorgi D, eds. Trustworthy Global Computing. Berlin/Heidelberg: Springer, 2005. 146–162 · Zbl 1151.68516
[33] Varacca D, Yoshida N. Probabilistic {\(\pi\)}-calculus and event structures. Electr Notes Theor Comput Sci, 2007, 190: 147–166 · Zbl 1279.68269 · doi:10.1016/j.entcs.2007.07.009
[34] Varacca D, Völzer H, Winskel G. Probabilistic event structures and domains. Theor Comput Sci, 2006, 358: 173–199 · Zbl 1099.68054 · doi:10.1016/j.tcs.2006.01.015
[35] Sangiorgi D, Walker D. The {\(\pi\)}-calculus: A Theory of Mobile Processes. Cambridge: Cambridge University Press, 2001 · Zbl 0981.68116
[36] Larsen K G, Skou A. Bisimulation through probabilistic testing. Inf Comput, 1991, 94: 1–28 · Zbl 0756.68035 · doi:10.1016/0890-5401(91)90030-6
[37] Wu P, Palamidessi C, Lin H. Symbolic bisimulations for probabilistic systems. In: the 4th International Conference on the Quantitative Evaluation of Systems, Edinburgh, 2007. 179–188
[38] Parrow J. An introduction to the {\(\pi\)}-calculus. In: Bergstra J, Ponse A, Smolka S A, eds. Handbook of Process Algebra. Amsterdam-Lausanne-New York-Oxford-Shannon-Tokyo: Elsevier Science, 2001. 479–543 · Zbl 1035.68071
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.