Coalgebraic Tools for Bisimilarity and Decorated Trace Semantics

Abstract

One of the research areas of great importance in Computer Science is the study of the semantics of concurrent reactive systems. These are systems that compute by interacting with their environment, and typically consist of several parallel components, which execute simultaneously and potentially communicate with each other. Examples of such systems range from rather simple devices such as calculators and vending machines, to programs controlling mechanical devices such as cars, subways or spaceships. In light of their widespread deployment and complexity, the application of rigorous methods for the specification, design and reasoning on the behaviour of reactive systems has always been a great challenge. One possible approach to formally handle reactive systems is to use a “common language" for describing both the actual implementations and their specifications. When following this technique, verifying whether an implementation and its specification describe the same behaviour reduces to proving some notion of equivalence/ preorder between their corresponding descriptions over the chosen language. The aim of this thesis is to exploit the strengths of a (co)algebraic framework in modelling reactive systems and reasoning on several types of associated semantics, in a uniform fashion. Moreover, we derive a suite of corresponding verification algorithms suitable for implementation in automated tools. In Chapter 3 we present a decision procedure for bisimilarity of a class of expressions defining systems such as infinite streams, deterministic automata, Mealy machines and labelled transition systems. The procedure is implemented in the automatic theorem prover CIRC. Chapter 4 provides a uniform coalgebraic handling of a series of semantics on transition systems. This is achieved by employing a generalisation of the classical powerset construction for determinising non-deterministic automata. In particular, we deal with decorated trace equivalences for labelled transition systems and probabilistic systems and, (the so-called “must” and “may”) testing semantics for divergent non-deterministic systems. The coalgebraic approach enabled reasoning on the aforementioned notions of behavioural equivalence/preorder in terms of bisimulations. Moreover, our framework facilitated the construction of verification algorithms which are not available for bisimilarity, as shown in Chapter 5. There we provide a variation of Brzozowski’s algorithm to minimise finite automata and an optimisation of Hopcroft and Karp’s algorithm for language semantics. Both algorithms were successfully applied to reason on decorated trace and testing semantics. The corresponding implementations can be tested online at: http://perso.ens-lyon.fr/damien.pous/brz/.