Categorical algebras for the compositional construction of probabilistic and distributed systems.

Structured transition systems have been widely used in the formal specification of computing systems, including concurrent and probabilistic systems. In this thesis we extend the span of graphs algebra introduced in [40] to describe concurrent systems in a compositional way, in order to model probabilistic distributed systems. The span algebra of [40] may be regarded as an extension of various automata models of computation based on distributed automata. With the introduction of both parallel and sequential operations, this extension allows the compositional description of concurrent, distributed and mobile systems. An important aspect of span graph model is that there is also a geometric characterization associated with the algebra along the lines of Penrose’s algebra of tensors. The algebra of transition systems we describe is a well-supported compact closed category - a symmetric monoidal category for which every object has a separable algebra structure (satisfying Frobenius equation) - whose arrows are automata in which the actions have probabilities. The operations of the category permit the compositional description of probabilistic processes and in particular of classical finite Markov chains. The systems we can model with our algebra are distributed, hierarchical and with an evolving geometry. We also extend the span algebra of [40] in order to permit the inclusion of quantum components. Again, this algebra is a well-supported compact closed category. This extension permits a compositional description of quantum protocols, in which quantum components interact with classical finite state components. In our view, the inclusion of explicit components of finite state classical control adds conceptual clarity and precision to quantum protocols.