The seminar dealt with recent developments in the emerging area of coalgebraic logic and was the first Dagstuhl seminar on that topic. Coalgebraic logic is a branch of logic which studies coalgebras as models of systems and their logics. It can be seen as generalising and extending the classical theory of modal logic to more general models of systems than labelled transition systems. Traditionally, modal logics find their use when reasoning about behavioural and temporal properties of computation and communication, whereas coalgebras give a uniform account for a large class of different systems.

The seminar discussed foundational topics in a particular branch of logic, so problems which command a direct application in an industrial context were outside the seminar's scope. We expect, however, that specification methods related to coalgebraic logics will enter fields like model checking and other areas of industrial interest, once the mathematical foundations in this area are firmer and better understood.

The following glossary puts coalgebraic logic in its larger context.

Modal logic is a field with roots in philosophical logic and mathematics. As applied to computer science it has become central in order to reason about the behavioural and temporal properties of computing and communicating systems, as well as to model properties of agents such as knowledge, obligations, and permissions. Two of the reasons for the success of modal logic are the following. First, many modal logics are —despite their remarkable expressive power— decidable and, therefore, amenable to automated reasoning and verification. Second, Kripke’s relational semantics of modal logic turned out to be amazingly flexible, both in terms of providing techniques to prove properties of modal logics and in terms of allowing the different applications of modal logic to artificial intelligence, software agents, etc.

Coalgebra is a more recent area. Following on from Aczel’s seminal work on non-well founded set theory, coalgebra has been developed into a general theory of systems. The basic idea is that coalgebras are given with respect to a parameter F. Different choices of F yield, for example, the Kripke frames and models of modal logic, the labelled transition systems of process algebra, the deterministic automata of formal language theory, or the Markov chains used in statistics. Rutten showed that, in analogy with universal algebra, a theory of systems, called universal coalgebra, can be built uniformly in the parameter F, simultaneously covering the above and other examples. Crucial notions such as behavioural equivalence observational equivalence, bisimilarity), final semantics and coinduction find their natural place here.

Coalgebraic logic combines coalgebra and modal logic to study logics of systems uniformly in the parameter F. Given the plethora of different transition systems and their ad hoc logics, such a uniform theory is clearly desirable. Uniformity means that results on, for example, completeness, expressivity, finite model property and complexity of satisfiability can be established at once for all functors (possibly satisfying some, usually mild, conditions). Additionally, there is also a concern for modularity: Typically, a parameter F is composed of basic features (such as input, output, non-determinism, probability). Modularity then means that the syntax/proof systems/algorithms for the logic of F are obtained compositionally from the syntax/proof systems/algorithms for the logics of the basic features.

When we planned the seminar, we envisaged six broad topics. We indicate which of the talks fall under which topic.

1. Category Theoretic Aspects of Coalgebraic Logic
2. Probabilistic Transition Systems
3. Stone Duality
4. Coalgebraic Logic, Automata Theory, Fixed Point Logics
5. Coalgebraic Logic for Structural Operational Semantics
6. Applied Coalgebraic Logic

Moss gave a presentation on new developments on the logic of recursion, which is one of the oldest topics in coalgebraic logic going back to the book Vicious Circles by Barwise and Moss (1996). New perspectives for coalgebraic logic where opened by the talks by Abramsky and Jacobs (quantum systems), and Pavlovic (security).