Coalgebraic modelling: Applications in automata theory and modal logic

In this thesis we apply coalgebraic modelling to gain new insights into automata theory and modal logic. Briefly summarised, the main contributions consist of (i) a coalgebraic technique for synthesising Mealy machines from arithmetic bitstream specifications, and results that relate Mealy machines to rational specifications in terms of expressivity and complexity; (ii) a coalgebraic perspective on subsequential transducers, and a systematic classification of reflective subcategories of subsequential structures; (iii) bisimulation notions for neighbourhood structures and model theoretic results for classical modal logic, including interpolation and a characterisation of classical modal logic as the bisimulation invariant fragment of first order logic. These contributions are found in Chapters 3, 4 and 5. In Chapter 3 we study the relationship between bitstream functions and Mealy machines with binary input and output. Mealy machines and binary arithmetic play an important role in the modelling and specification of sequential circuits. It is well-known that Mealy machines can be modelled as coalgebras and that a final Mealy coalgebra exists. We present a method which given a so-called rational specification of an arithmetic bitstream function constructs a Mealy machine which realises the specification. The idea behind the construction is to define a Mealy structure on the set of specifications, and construct a realisation as the submachine generated by the given specification. Termination and minimality are ensured by working modulo bisimilarity. This method is essentially coalgebraic since the idea, in principle, applies to other coalgebra types and specification languages. In our case, we obtain a Mealy structure on the set of specifications by defining the arithmetic operations coinductively, and we determine bisimilarity of specifications by reduction to normal form. We have implemented this construction method and we give a complexity analysis of the algorithm. Furthermore, we present upper bounds on the number of states in the constructed Mealy machine, and we show that there exist finite Mealy machines that are not the realisation of a rational specification. In Chapter 4 we focus on the coalgebraic modelling of subsequential transducers. Subsequential transducers are a type of automata which combines transduction with acceptance, and they are used in the areas of coding theory and language processing. As a class of automata they generalise Mealy machines and classical deterministic automata, both of which have a neat coalgebraic modelling. The underlying structure of a subsequential transducer also looks like a coalgebra, however, it is quite easy to see that the corresponding notion of coalgebra morphism does not fit well with the intended word function semantics. We show that a proper coalgebraic modelling can be obtained for the subclass of normalised subsequential structures. This result provides a new perspective on known results such as the existence of canonical minimal subsequential transducers, and the fact that subsequential transducers can be minimised by first normalising and then identifying bisimilar states. We also show that normalisation, minimisation and taking differentials are reflectors in the category theoretic sense. In Chapter 5, our starting point is the coalgebraic modelling of neighbourhood structures. Neighbourhood structures are the standard semantic tool used for reasoning about non-normal modal logics. The modal logic of all neighbourhood models is called ‘classical modal logic’. Neighbourhood models generalise Kripke models, but they have received far less attention. In particular, so far a notion of bisimulation was lacking. We apply the coalgebraic modelling to define three notions of state equivalence in neighbourhood structures. One of these is a new coalgebraic notion which lies in between bisimilarity and behavioural equivalence. In the modal logic of Kripke models, the close relationship between bisimilarity and the expressivity of the modal language is known from results such as the Hennessy-Milner theorem and Van Benthem’s characterisation theorem. We prove analogues of these results for classical modal logic, and we give a model theoretic proof of Craig interpolation in which coalgebraic bisimulations play a central role