Probabilistic Methods in Concurrency
(Concurrent Languages for Probabilistic Asynchronous Communication)
PhD Course, Pisa, 28/6  15/7/2004
[ Lectures ]
[ Bibliography ]
[ Exam ]
 The picalculus and the asynchronous picalculus. Lecture notes (ppt , pdf).
 The picalculus hierarchy: encodings. Lecture notes (ppt , pdf).
 Encoding of input guarded choice in the asynchonous picalculus
 Encoding of output prefix in the asynchonous picalculus
 The picalculus hierarchy: separation results (ppt , pdf).
 Separation between the picalculus and the asynchonous picalculus
 Separation between the picalculus 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 ,
pdf).
 A tool for verification of probabilistic automata: Progress Statements (ppt ,
pdf).
 The probabilistic picalculus (ppt ,
pdf).
 Encoding of the picalculus into the probabilistic asynchronous picalculus (ppt ,
pdf).
 Other uses of randomization: a randomized protocol for anonymity (ppt ,
pdf).
 A proof search specification of the picalculus (speaker: Dale Miller) (pdf).
 Robin Milner.
Communicating and mobile systems: the picalculus.
Cambridge University Press, 1999 (Lecture 1).
 Joachim Parrow. An Introduction to the piCalculus.
In Handbook of Process Algebra, ed.
Bergstra, Ponse, Smolka, pages 479543, Elsevier 2001.
BRICS RS 9942 (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 picalculus. A Theory of Mobile Processes.
Cambridge University Press, 2001 (Lecture 1).
 Gerard Boudol,
Asynchrony and the picalculus,
INRIA Research Report 1702, 1992 (Lecture 2).
 Diletta Cacciagrano, Flavio Corradini, Catuscia Palamidessi.
On the impossibility of encoding synchronous communication in
asynchronous picalculus 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.133147, SpringerVerlag, 1991 (Lecture 2).
 Uwe Nestmann and
Benjamin Pierce,
Decoding Choice Encodings.
Journal of Information & Computation163(1): 159, 2000.
Report version
BRICS RS 9942 (Lecture 2).
 Catuscia Palamidessi.
Comparing the Expressive Power of the
Synchronous and the Asynchronous
picalculus. Mathematical Structures in Computer Science, 13(5): 685719, 2003.
(pdf,
ps.)
A preliminary version appeared in the Proc. of the 24th
ACM Symposium on Principles of Programming
Languages (POPL), pages 256265, 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 SIGPLANSIGACT symposium on Principles of programming languages, 1981 (Lecture 4).
 YuhJzer 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): 287309, 2001 (Lecture 5).
 Prakash Panangaden, Stochastic techniques in Concurrency.
Lecture notes (Lecture 5).
 R. Segala, Modeling and Verification of Randomized Distributed RealTime Systems,
PhD thesis, Laboratory for Computer Science, Massachusetts Institute of Technology,
June 1995. Available as Technical Report MIT/LCS/TR676
(ToC ,
1 ,
2 ,
3) (Lectures 5 and 6).
 Roberto Segala and Nancy Lynch.
Probabilistic simulations for probabilistic processes.
Nordic Journal of Computing, 2(2):250273, 1995.
An extended abstract appeared in the Proceedings of CONCUR '94,
LNCS 836: 2225. (Lectures 5 and 6).

O.M. Herescu, C. Palamidessi.
Probabilistic asynchronous picalculus.
In J. Tiuryn, ed., Proc. of FOSSACS 2000
(Part of ETAPS 2000), vol. 1784 of
LNCS, pages 146160. SpringerVerlag, 2000.
(ps,
ps of report version.) (Lecture 7).
 Mihaela Herescu.
The Probabilistic Asynchronous picalculus. PhD Thesis (ps ,
 pdf) (Lectures 7 and 8)
 A
distributed implementation of the probabilistic asynchronous picalculus (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 8189, ACM, 2001 (Lecture 8).
(ps.)

C. Palamidessi, O.M. Herescu.
A Randomized Distributed Encoding of the PiCalculus with Mixed
Choice.
Proc. of IFIPTCS 2002, pages 537549, 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 198218. 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 picalculus.
Technical report (Local copy.) (Lecture 10).
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.
List of exercises
 [5 points]
Show two picalculus 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 HondaTokoro of the output prefix into the asynchronous picalculus. 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 picalculus, or Milner's book on the picalculus. 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 picalculus and the asynchronous picalculus? 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 SegalaLynch (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 picalculus. (Ref. Lecture 7).
 [10 points] Consider the following process in probabilistic asynchronous picalculus (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
 every fair scheduler,
 every scheduler
Justify your answers. (Cfr. Lectures 7 and 8.)