Probabilistic Methods in Concurrency
(Concurrent Languages for Probabilistic Asynchronous Communication)
PhD Course, Pisa, 28/6 - 15/7/2004
[ Lectures ]
[ Bibliography ]
[ Exam ]
- The pi-calculus and the asynchronous pi-calculus. Lecture notes (ppt , pdf).
- 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
- 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
- Problems in distributed systems for which only randomized
solutions exists (ppt , pdf).
- Basics of Measure Theory and Continuous Probability Theory.
Probabilistic Automata (ppt ,
- A tool for verification of probabilistic automata: Progress Statements (ppt ,
- The probabilistic pi-calculus (ppt ,
- Encoding of the pi-calculus into the probabilistic asynchronous pi-calculus (ppt ,
- Other uses of randomization: a randomized protocol for anonymity (ppt ,
- A proof search specification of the pi-calculus (speaker: Dale Miller) (pdf).
The exam consists in solving some exercises of the list enclosed below.
Each exercises is worth a number of points. You can select the exercises you want, up to 20 points (if you solve more than 20 points exercises, the score will be anyway renormalized to 20).
Please send me the solution by email by September 30, 2004.
- 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
Decoding Choice Encodings.
Journal of Information & Computation163(1): 1-59, 2000.
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.
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
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 of report version.) (Lecture 7).
- Mihaela Herescu.
The Probabilistic Asynchronous pi-calculus. PhD Thesis (ps ,
| pdf) (Lectures 7 and 8)
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).
C. Palamidessi, O.M. Herescu.
A Randomized Distributed Encoding of the Pi-Calculus with Mixed
Proc. of IFIP-TCS 2002, pages 537-549, Kluwer, 2002.
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.
- 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
Foundational Aspects of Syntax.
ACM Computing Surveys, 31(3es):11, 1999.
(ps) (Lecture 10).
Dale Miller and
A Proof Search specification of the pi-calculus.
Technical report (Local copy.) (Lecture 10).
List of exercises
- [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.)
- [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.)
- [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.)
- [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 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).
- [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).
- [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 = recA (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
Justify your answers. (Cfr. Lectures 7 and 8.)
- every fair scheduler,
- every scheduler