Samenvatting
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 wellknown that Mealy machines can be modelled as coalgebras and that a final Mealy coalgebra exists. We present a method which given a socalled 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 nonnormal 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 HennessyMilner 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.
Originele taal2  Engels 

Kwalificatie  Doctor in de Filosofie 
Toekennende instantie 

Begeleider(s)/adviseur 

Datum van toekenning  14 mei 2009 
Plaats van publicatie  Amsterdam 
Uitgever  
Gedrukte ISBN's  9789086593088 
Status  Gepubliceerd  2009 
Vingerafdruk Duik in de onderzoeksthema's van 'Coalgebraic modelling: Applications in automata theory and modal logic'. Samen vormen ze een unieke vingerafdruk.
Citeer dit
Hansen, H. H. (2009). Coalgebraic modelling: Applications in automata theory and modal logic. Vrije Universiteit Amsterdam.