 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


Statebased 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 statebased 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, evergrowing 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 conduction • (generalized) power set construction • induction and coinduction • coalgebraic language equivalence • behavioural equivalence • universal coalgebra 
The participants will be graded based on homework assignments and a final exam. The final grade will be the maximum of (H+E)/2 and E, 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 and modal logic, the course will be selfcontained: Only basic definitions will be needed, and these will be introduced as part of the course. 


The course material will consist of slides, handouts, and research papers on coalgebra. All material will be made available electronically via the course website, or distributed during the course. To get an impression of the course topic, we refer to the following articles: • [JR12, Rut00, Rut98, Rut05, Ven06]. • [JR12] 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. • [Rut00] J.J.M.M. Rutten. Universal coalgebra: a theory of systems. Theoret. Comput. Sci., 249(1):3  80, 2000. • [Rut98] 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. 194218. • [Rut05] J.J.M.M. Rutten. A tutorial on coinductive stream calculus and signal flow graphs.. Theoret. Comput. Sci., 343(3):443  481, 2005. • [Ven06] Y. Venema. Algebras and coalgebras. In P. Blackburn, J. van Benthem, and F. Wolter, editors, Handbook of Modal Logic, volume 3 of Studies in Logic and Practical Reasoning, pages 331  426. Elsevier, 2006. 

• 32 hours lecture • 32 hours problem session • 136 hours individual study period Extra information teaching methods: 
  Verplicht materiaalHandoutsThe course material will consist of slides, handouts, and research papers on coalgebra.
All material will be made available electronically via the course website, or distributed during the course. 

 Aanbevolen materiaalArtikelenB. 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. 
 ArtikelenJ.J.M.M. Rutten. A tutorial on coinductive stream calculus and signal flow graphs.. Theoret. Comput. Sci., 343(3):443  481, 2005. 
 ArtikelenJ.J.M.M. Rutten. Universal coalgebra: a theory of systems. Theoret. Comput. Sci., 249(1):3  80, 2000. 
 ArtikelenJ.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. 194218. 
 ArtikelenY. Venema. Algebras and coalgebras. In P. Blackburn, J. van Benthem, and F. Wolter, editors, Handbook of Modal Logic, volume 3 of Studies in Logic and Practical Reasoning, pages 331  426. Elsevier, 2006. 

 WerkvormenCursus
 Hoorcollege
 Werkcollege
 Zelfstudie

 ToetsenTentamenWeging   1 
Toetsvorm   Tentamen 
Gelegenheden   Blok KW2, Blok KW3 


 