Abstract
We propose an extension of the asynchronous π-calculus with a notion of random choice. We define an operational semantics which distinguishes between probabilistic choice, made internally by the process, and nondeterministic choice, made externally by an adversary scheduler. This distinction will allow us to reason about the probabilistic correctness of algorithms under certain schedulers. We show that in this language we can solve the electoral problem, which was proved not possible in the asynchronous π-calculus. Finally, we show an implementation of the probabilistic asynchronous π-calculus in a Java-like language.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
R. Amadio, I. Castellani, and D. Sangiorgi. On bisimulations for the asynchronous π-calculus. TCS, 195(2):291–324, 1998.
G. Boudol. Asynchrony and the π-calculus (note). Rapport de Recherche 1702, INRIA, Sophia-Antipolis, 1992.
O. M. Herescu and C. Palamidessi. Probabilistic asynchronous π calculus. Tech. Rep., Dept. of Comp. Sci. and Eng., Penn State Univ., 2000. Postscript available at http://cse.psu.edu/~catuscia/papers/prob_impl/report2.ps.
K. Honda and M. Tokoro. An object calculus for asynchronous communication. In Proc. of ECOOP, volume 512 of LNCS, pages 133–147. Springer-Verlag, 1991.
R. Milner. Communicating and mobile systems: the π-calculus. Cambridge University Press, 1999.
R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, I and II. Inf. and Comp., 100(1):1–40 & 41–77, 1992.
U. Nestmann. On the expressive power of joint input. In EXPRESS’ 98, volume 16.2 of Electronic Notes in TCS. Elsevier Science B.V., 1998.
U. Nestmann and B. Pierce. Decoding choice encodings. In Proc. of CONCUR’ 96, volume 1119 of LNCS, pages 179–194. Springer-Verlag, 1996.
C. Palamidessi. Comparing the expressive power of the synchronous and the asynchronous π-calculus. In Conference Record of POPL’ 97, pages 256–265, 1997.
M. O. Rabin and D. Lehmann. On the adantages of free choice: A symmetric and fully distributed solution to the dining philosophers problem. In A Classical Mind: Essays in Honour of C.A.R. Hoare, chapter 20, pages 333–352. Prentice Hall, 1994.
R. Segala. Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, MIT, June 1995. Tech. Rep. MIT/LCS/TR-676.
R. Segala and N. Lynch. Probabilistic simulations for probabilistic processes. Nordic Journal of Computing, 2(2):250–273, 1995.
M. Y. Vardi. Automatic verification of probabilistic concurrent finite-state programs. In Proc. of FOCS, pages 327–338. IEEE, 1985.
W. Yi and K. G. Larsen. Testing probabilistic and nondeterministic processes. In Proc. of the 12th IFIP Int.l Symp. on Protocol Specification, Testing and Verification. North Holland, 1992.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Herescu, O.M., Palamidessi, C. (2000). Probabilistic Asynchronous π-Calculus. In: Tiuryn, J. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2000. Lecture Notes in Computer Science, vol 1784. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46432-8_10
Download citation
DOI: https://doi.org/10.1007/3-540-46432-8_10
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67257-9
Online ISBN: 978-3-540-46432-7
eBook Packages: Springer Book Archive