Systems, Automata, and Coalgebras

A course by Lutz Schröder at the Universität Bremen 2004.

Depending on the nature of the program at hand, there are two fundamentally different notions of correctness: on the one hand, there are programs that are supposed to terminate and produce a correct result; on the other hand, there are programs that are expected to run essentially forever and correctly interact with their environment during execution. Programs of the latter type are often referred to as reactive systems. Typical simple examples are automatic teller machines and vending machines, but also operating systems and demons. Correctness requirements for reactive systems generally concern properties of the states that the system can reach, as well as the temporal and local patterns of states, as in `the ATM will dispense money only if the correct PIN has been typed in' or `upon insertion of a one-Euro-coin, the coffee vending machine will provide a cup of coffee after a finite period of waiting'.

Interestingly, the two types of programs just mentioned are, w.r.t. their abstract treatment, duals of each other: while the input/output behavior of a terminating program is typically described as an algebra (this is the object of algebraic specification), reactive systems have more recently been treated as so-called coalgebras. Here, the notion of coalgebra is in a precise sense the `opposite' of the notion of algebra. The course will be concerned with coalgebraic system theory in this sense, as well as with formalisms for expressing requirements on reactive systems.

Teaching Material

• Slides on LTS
• Lecture Notes on Formal Models of Concurrency by Horst Reichel, Dresden
• Slides on Simulation
• Slides on Minimization
• Slides on Morphisms
• Slides on finitely branching LTS and Sub-LTS
• Slides on generated Sub-LTS and Countability
• Slides on Disjoint Sums and the Second Homomorphism Theorem
• Slides on Corecursion and Coinduction
• Slides on Hennessy/Milner Logic
• Slides on Coalgebraic Bisimulation
• Lecture Notes on Coalgebras and Modal Logic by Alexander Kurz
• Jan Rutten: Automata and Coinduction (an exercise in coalgebra)
• Bart Jacobs and Jan Rutten: A Tutorial on (Co)Algebra and (Co)Induction
• Bart Jacobs: Exercises in Coalgebraic Specification
• Problem Sheet 1
• Problem Sheet 2
• Problem Sheet 3