Axiomatisations and Types for Probabilistic and Mobile Processes

                                                   Yuxin Deng


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 reasoning.