Axiomatisations and Types for Probabilistic and Mobile Processes
Was successfully defended on July 22, 2005
(Mention Très Honorable)
175 rue du Chevaleret, Paris 13ème.
Rez-de-chaussée, salle 0C2
Roberto Di Cosmo
Matthew Hennessy (reviewer)
Roberto Segala (reviewer)
The focus of this thesis are the theoretical foundations for reasoning about
algorithms and protocols for modern distributed systems. Two important
features of models for these systems are probability and typed
mobility: probabilities can be used to quantify
unreliable or unpredictable behaviour and types can be used to
guarantee secure behaviour in systems with a mobile structure.
In this thesis we develop algebraic and type-based techniques for
behavioural reasoning on probabilistic and mobile processes.
In the first part of the thesis we study the algebraic theory of a
process calculus which
combines both nondeterministic and
probabilistic behaviour in the style of Segala and Lynch's probabilistic
automata. We consider various strong and weak behavioural equivalences,
and we provide complete axiomatisations for finite-state processes,
restricted to guarded recursion in the case of the weak equivalences.
In the second part of the thesis we investigate the algebraic theory
of the $\pi$-calculus under the effect of capability types, which are
one of the most useful forms of types in mobile process calculi.
Capability types allow one to distinguish
between the capability to read from a channel, to write to a channel,
and to both read and write. They also
give rise to a natural and powerful subtyping relation.
We consider two variants of typed bisimilarity, both in their late and
in their early version. For both of them, we give complete
axiomatisations on the closed finite terms. For one of the two
variants, we provide a complete axiomatisation for the open finite terms.
In the last part of the thesis we develop a type-based technique for verifying
the termination property of some mobile processes. We provide four
type systems to guarantee this property.
The type systems are obtained by
successive refinements of the types of the simply typed $\pi$-calculus.
The termination proofs take advantage of techniques from term
rewriting systems. These type systems can be used for reasoning about the
terminating behaviour of some non-trivial
examples: the encodings of primitive recursive functions, the protocol
for encoding separate choice in terms of parallel composition, a
symbol table implemented as a dynamic chain of cells.
These results lay out the foundations for further
study of more advanced models which may
combine probabilities with types. They also highlight the
robustness of the algebraic and type-based techniques for behavioural
A short version (only in English) can be downloaded at [PS] and [PDF].
The full version, which also includes a resume in French, can be downloaded at [PS] and [PDF].