After successful completion of the course, the participants are able to:
- model streams and various types of automata as coalgebras
- apply coinduction as a proof- and definition principle for streams and automata
- apply the general coalgebraic definitions of behavior and equivalence to concrete system types
- understand and use basic concepts from category theory
State-based systems are used widely in computer science to model concrete systems such as digital hardware, software programs, and distributed systems. Coalgebra is a unifying framework for studying the behaviour of state-based systems. In coalgebra, a system is viewed as a black box where knowledge of the system’s state can only be obtained by observing the external behaviour. In particular, two states s and t are considered equivalent if whenever we run the system starting in state s, the observed behaviour is the same as when we run the system in starting in state t.
The type of observations and transitions in the external behaviour is specified by the system type. The theory of universal coalgebra provides general definitions of observable behaviour and bisimilarity that can be instantiated for concrete system types, as well as a powerful and fascinating reasoning principle called coinduction (a notion that is dual to the well known induction principle).
This course is an introduction to coalgebra. The course starts by studying how various types of systems can be modelled as coalgebras, and how coinduction can be applied to them. These systems include basic datatypes, such as infinite streams and trees, and many types of automata (deterministic, nondeterministic, probabilistic, ...). Next, a number of fundamental notions such as language equivalence of automata, bisimilarity of processes and determinisation of nondeterministic automata, will be treated coalgebraically. The students will learn how to combine coinduction and induction to derive effective specification and reasoning techniques for automata. The coalgebraic framework will then be used to obtain generalisations of these constructions to other types of systems.
Coalgebra is a rather recent field of research, existing for a mere two decades, and it is attracting an enthusiastic, ever-growing community. Being relatively young, it still has many elementary and exciting research questions to offer.
|This course fits well in a program that includes one or more of the following: Category Theory, Semantiek en Correctheid, Semantics and Domain Theory, Universal Algebra, Model Theory, Proof assistants, Analysis of Embedded Systems.|
|• infinite streams|
• automata and coinduction
• induction and coinduction
• coalgebraic language equivalence
• behavioural equivalence
• universal coalgebra
• categories, functors
|The participants will be graded based on homework assignments and a final exam. The final grade is computed as (H+E)/2, where H is the grade given for the homework assignments and E is the grade given for the final exam.|
|We only assume basic knowledge of automata, formal languages and propositional logic. |
For example, as covered in the courses: Talen en Automaten, Discrete Wiskunde, Beweren & Bewijzen, en Semantiek & Correctheid.
With respect to category theory, the course will be self-contained: only basic definitions will be needed, and these will be introduced as part of the course.
|The course material will consist of hand-outs and research papers on coalgebra.
All material will be made available electronically via the course website, or distributed during the course.|Aanbevolen materiaal
|B. Jacobs and J.J.M.M. Rutten. An introduction to (co)algebra and (co)induction. In D. Sangiorgi and J.J.M.M. Rutten, editors, Advanced Topics in Bisimulation and Coinduction, Cambridge University Press, 2012.|
|J.J.M.M. Rutten. A tutorial on coinductive stream calculus and signal flow graphs.. Theoret. Comput. Sci., 343(3):443 - 481, 2005.|
|J.J.M.M. Rutten. Universal coalgebra: a theory of systems. Theoret. Comput. Sci., 249(1):3 - 80, 2000.|
|J.J.M.M. Rutten. Automata and coinduction (an exercise in coalgebra). Proceedings of CONCUR '98, D. Sangiorigi and R. de Simone (eds.), LNCS 1466, Springer, 1998, pp. 194-218.|
|B. Jacobs, Introduction to Coalgebra. Towards Mathematics of States and Observations. Cambridge Univ. Press, 2016|
|Gelegenheden||Blok KW2, Blok KW3|