Coalgebraic modelling: Applications in automata theory and modal logic

H.H. Hansen

Research output: ThesisPhd Thesis 4 Research NOT TU/e / Graduation NOT TU/e)

3 Downloads (Pure)

Abstract

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.
Original languageEnglish
QualificationDoctor of Philosophy
Awarding Institution
  • Vrije Universiteit Amsterdam
Supervisors/Advisors
  • Rutten, J.J.M.M., Promotor, External person
  • Venema, Y., Copromotor, External person
  • Kupke, C.A., Copromotor, External person
Award date14 May 2009
Place of PublicationAmsterdam
Publisher
Print ISBNs978-90-865930-8-8
Publication statusPublished - 2009

Fingerprint

Automata Theory
Modal Logic
Specification
Transducer
Coalgebra
Modeling
Bisimulation
Classical Logic
Kripke Models
Automata
Interpolate
Equivalence
Binary
Arithmetic Functions
Generalise
Coding Theory
Characterization Theorem
Complexity Analysis
Minimality
Specification Languages

Cite this

Hansen, H. H. (2009). Coalgebraic modelling: Applications in automata theory and modal logic. Amsterdam: Vrije Universiteit Amsterdam.
Hansen, H.H.. / Coalgebraic modelling: Applications in automata theory and modal logic. Amsterdam : Vrije Universiteit Amsterdam, 2009. 194 p.
@phdthesis{2afb364094844ab0999112597c385a45,
title = "Coalgebraic modelling: Applications in automata theory and modal logic",
abstract = "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.",
author = "H.H. Hansen",
year = "2009",
language = "English",
isbn = "978-90-865930-8-8",
publisher = "Vrije Universiteit Amsterdam",
school = "Vrije Universiteit Amsterdam",

}

Hansen, HH 2009, 'Coalgebraic modelling: Applications in automata theory and modal logic', Doctor of Philosophy, Vrije Universiteit Amsterdam, Amsterdam.

Coalgebraic modelling: Applications in automata theory and modal logic. / Hansen, H.H.

Amsterdam : Vrije Universiteit Amsterdam, 2009. 194 p.

Research output: ThesisPhd Thesis 4 Research NOT TU/e / Graduation NOT TU/e)

TY - THES

T1 - Coalgebraic modelling: Applications in automata theory and modal logic

AU - Hansen, H.H.

PY - 2009

Y1 - 2009

N2 - 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.

AB - 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.

UR - http://hdl.handle.net/1871/13247

M3 - Phd Thesis 4 Research NOT TU/e / Graduation NOT TU/e)

SN - 978-90-865930-8-8

PB - Vrije Universiteit Amsterdam

CY - Amsterdam

ER -

Hansen HH. Coalgebraic modelling: Applications in automata theory and modal logic. Amsterdam: Vrije Universiteit Amsterdam, 2009. 194 p.