February 3, 2015
Andrea Cerone
I propose a process calculus to model high-level distributed systems, whose topology is described by a digraph. The calculus enjoys interesting features, such as probabilistic behaviour and broadcast communication. I first focus on the problem of composing distributed systems, then I present a compositional theory based on a probabilistic generalisation of the de Nicola’s and Hennessy’s testing preorders.
Also, I define an extensional semantics for our calculus, which will be used to define both simulation and deadlock simulation preorders for distributed systems. I prove that the simulation preorder is sound with respect to the may-testing preorder; similarly, the deadlock simulation preorder is sound with respect to the must-testing preorder, for a large class of networks. I also provide a counterexample showing that completeness of the may testing preorder does not hold. I conclude the presentation with two simple applications of the developed theory: a probabilistic routing protocol and a virtual shared memory system.