Probabilistic Methods in Concurrency

(Concurrent Languages for Probabilistic Asynchronous Communication)

PhD Course, Pisa, 28/6 - 15/7/2004

Catuscia Palamidessi

Lectures

1. The pi-calculus and the asynchronous pi-calculus. Lecture notes (ppt , pdf).

2. The pi-calculus hierarchy: encodings. Lecture notes (ppt , pdf).

   • Encoding of input guarded choice in the asynchonous pi-calculus

   • Encoding of output prefix in the asynchonous pi-calculus

3. The pi-calculus hierarchy: separation results (ppt , pdf).

   • Separation between the pi-calculus and the asynchonous pi-calculus

   • Separation between the pi-calculus and CCS

4. Problems in distributed systems for which only randomized solutions exists (ppt , pdf).

5. Basics of Measure Theory and Continuous Probability Theory. Probabilistic Automata (ppt , pdf).

6. A tool for verification of probabilistic automata: Progress Statements (ppt , pdf).

7. The probabilistic pi-calculus (ppt , pdf).

8. Encoding of the pi-calculus into the probabilistic asynchronous pi-calculus (ppt , pdf).

9. Other uses of randomization: a randomized protocol for anonymity (ppt , pdf).

10. A proof search specification of the pi-calculus (speaker: Dale Miller) (pdf).

Bibliography

• Robin Milner. Communicating and mobile systems: the pi-calculus. Cambridge University Press, 1999 (Lecture 1).

• Joachim Parrow. An Introduction to the pi-Calculus. In Handbook of Process Algebra, ed. Bergstra, Ponse, Smolka, pages 479-543, Elsevier 2001. BRICS RS 99-42 (Lecture 1).

• Benjamin Pierce. Foundational Calculi for Programming Languages. Chapter in the CRC Handbook of Computer Science and Engineering, 1996 (Lecture 1).

• Davide Sangiorgi and David Walker. The pi-calculus. A Theory of Mobile Processes. Cambridge University Press, 2001 (Lecture 1).

• Gerard Boudol, Asynchrony and the pi-calculus, INRIA Research Report 1702, 1992 (Lecture 2).
• Diletta Cacciagrano, Flavio Corradini, Catuscia Palamidessi. On the impossibility of encoding synchronous communication in asynchronous pi-calculus preserving testing semantics. Technical report, 2004 (Lecture 2).

• Kohei Honda and Mario Tokoro, An Object Calculus for Asynchronous Communication. Proc. of ECOOP'91, LNCS 512, pp.133-147, Springer-Verlag, 1991 (Lecture 2).

• Uwe Nestmann and Benjamin Pierce, Decoding Choice Encodings. Journal of Information & Computation163(1): 1-59, 2000. Report version BRICS RS 99-42 (Lecture 2).

• Catuscia Palamidessi. Comparing the Expressive Power of the Synchronous and the Asynchronous pi-calculus. Mathematical Structures in Computer Science, 13(5): 685-719, 2003. (pdf, ps.) A preliminary version appeared in the Proc. of the 24th ACM Symposium on Principles of Programming Languages (POPL), pages 256-265, ACM, 1997 (Lecture 3).
• Daniel Lehmann and Michael O. Rabin, On the andvantages of free choice: a symmetric and fully distributed solution to the dining philosophers problem. Proceedings of the 8th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, 1981 (Lecture 4).

• Yuh-Jzer Joung, Scott A. Smolka, Strong Interaction Fairness via Randomization. IEEE Transactions on Parallel and Distributed Systems, 1996 (Lecture 4).

• Prakash Panangaden, Measure and probability for concurrency theorists. TCS. 253(2): 287-309, 2001 (Lecture 5).

• Prakash Panangaden, Stochastic techniques in Concurrency. Lecture notes (Lecture 5).

• R. Segala, Modeling and Verification of Randomized Distributed Real-Time Systems, PhD thesis, Laboratory for Computer Science, Massachusetts Institute of Technology, June 1995. Available as Technical Report MIT/LCS/TR-676 (ToC , 1 , 2 , 3) (Lectures 5 and 6).

• Roberto Segala and Nancy Lynch. Probabilistic simulations for probabilistic processes. Nordic Journal of Computing, 2(2):250--273, 1995. An extended abstract appeared in the Proceedings of CONCUR '94, LNCS 836: 22--25. (Lectures 5 and 6).

• O.M. Herescu, C. Palamidessi. Probabilistic asynchronous pi-calculus. In J. Tiuryn, ed., Proc. of FOSSACS 2000 (Part of ETAPS 2000), vol. 1784 of LNCS, pages 146--160. Springer-Verlag, 2000.
(ps, ps of report version.) (Lecture 7).
• Mihaela Herescu. The Probabilistic Asynchronous pi-calculus. PhD Thesis (ps , | pdf) (Lectures 7 and 8)

• A distributed implementation of the probabilistic asynchronous pi-calculus (Lectures 7 and 8)

• O.M. Herescu, C. Palamidessi. On the Generalized Dining Philosophers Problem. Proc. of the 20th ACM Symposium on Principles of Distributed Computing (PODC) , pages 81-89, ACM, 2001 (Lecture 8). (ps.)
• C. Palamidessi, O.M. Herescu. A Randomized Distributed Encoding of the Pi-Calculus with Mixed Choice. Proc. of IFIP-TCS 2002, pages 537-549, Kluwer, 2002. (ps, ps of report version.) (Lecture 8).
• S. Schneider and A. Sidiropoulos, CSP and Anonymity. In Proc. of the European Symposium on Research in Computer Security (ESORIC'96), volume 1146 of Lecture Notes in Computer Science, pages 198--218. SpringerVerlag, 1996. (Lecture 9).

• Even, S., Goldreich, O., and Lempel, A, A randomized protocol for signing contracts. Communications of the ACM, 28(6), 637 - 647, 1985 (Lecture 9).

• Dale Miller and Catuscia Palamidessi. Foundational Aspects of Syntax. ACM Computing Surveys, 31(3es):11, 1999. (ps) (Lecture 10).
• Dale Miller and Alwen Tiu. A Proof Search specification of the pi-calculus. Technical report (Local copy.) (Lecture 10).

Exam

List of exercises

1. [5 points] Show two pi-calculus processes, P and Q, which are early bisimilar but not late bisimilar. P and Q must be written using only prefix, parallel, sum, and 0. (Ref. Lecture 1.)

2. [10 points] Let [[]] be the encoding of Honda-Tokoro of the output prefix into the asynchronous pi-calculus. Say whether this encoding is fully abstract wrt weak bisimulation. Namely, say whether it is true that P is weakly bisimilar to Q iff and only if [[P]] is weakly bisimilar to [[Q]]. Justify your answer. (Ref. Lecture 2.)
   For the definition of weak bisimilarity see, for instance, Sangiorgi and Walker's book on the pi-calculus, or Milner's book on the pi-calculus. For this exercise the difference between early and late is unessential.)

3. [5 points] Modify the definition of the Leader Election Problem in such a way that it is only the winner to output the result (the name of the winner), while the losers don't do aything. Does this version of the problem still separates the pi-calculus and the asynchronous pi-calculus? Justify your answer. (Ref. Lecture 3.)

4. [10 points] Consider Lehmann e Rabin's randomized algorithm for the dining philosophers. Consider the following modification: In line 3, replace goto 3 with goto 2. Namely, instead of doing busy waiting on the selected fork (first fork), the philosopher goes back and redo the random choice. Say whether this algorithm is still correct, i.e. whether it ensures with probability 1 that, for every fair scheduler, if a philosophe is hungy, then eventually a philosopher will eat. Also, answer the same question for unfair schedulers. Justify your answer using the progress statements of Segala-Lynch (Ref. Lectures 4 and 6.)

5. [5 points] Consider a finite set X, let Sigma be the set of all powersets of X, and define the function mu : Sigma -> [0,1] as mu(A) = #(A)/#(X), where #(A) is the cardinality of A. Is (X, Sigma, mu) a probability measure space? Justify your answer. (Ref. Lecture 5).

6. [5 points] Consider the randomized algorithm for the dining cryptographers (Ref. Lecture 9). Write this algorithm using the probabilistic asynchronous pi-calculus. (Ref. Lecture 7).

7. [10 points] Consider the following process in probabilistic asynchronous pi-calculus (where x^y represents the action of sending on x the name y:

   P = rec_A (1/2 tau . A + 1/2 tau . x^y)

   Consider the following tester

   T = tau . x(z) . omega

   Say whether P must T with probability 1, or not, for
   1. every fair scheduler,
   2. every scheduler
   Justify your answers. (Cfr. Lectures 7 and 8.)