Axiomatisations and Types for Probabilistic and Mobile Processes

Abstract

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.