The probabilistic asynchronous pi-calculus

by 1975- Herescu, Oltea Mihaela

iii In this dissertation, we consider a distributed implementation of the ?-calculus, more precisely, the version of the ?-calculus with mixed choice. To this end, we present the probabilistic asynchronous ?-calculus, which is an extension of the asynchronous ?- calculus enhanced 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. We propose a randomized distributed encoding of the ?-calculus, using the probabilistic asynchronous ?-calculus, and we show that our solution is correct with probability 1 under any proper adversary with respect to a notion of testing semantics. Finally, in order to prove that the probabilistic asynchronous ?-calculus is a sensible paradigm for the specification of distributed algorithms, we define a distributed implementation of the synchronization-closed probabilistic asynchronous ?-calculus in the Java language.