Dagstuhl Seminar 09502
( Dec 06 – Dec 09, 2009 )
- Ernst-Erich Doberkat (TU Dortmund, DE)
- Alexander Kurz (University of Leicester, GB)
- Annette Beyer (for administrative matters)
- Coalgebraic Logic : Special Issue : pp. 171-509 - Doberkat, Ernst-Erich; Kurz, Alexander - Cambridge : Cambridge Univ.. Pr., 2011 - (Mathematical structures in computer science : 21. 2011, 2).
- Collection of abstracts for the Dagstuhl-Seminar Coalgebraic Logic, December 6 - 9, 2009 - Battenfeld, Ingo; Doberkat, Ernst-Erich; Kurz, Alexander - Dortmund : Universität , 2009. - 14 S. - (Memo : Fakultät für Informatik : Lehrstuhl für Software-Technologie ; 181).
- Probabilistic Logical Characterization : article : pp. 154-172 - Hermanns, Holger; Parma, Augusto; Segala, Roberto; Wachter, Björn; Zhang, Lijun - Amsterdam : Elsevier, 2010 - (Information and Compuation : 209. 2010, pp. 154-172).
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.
- Category Theoretic Aspects of Coalgebraic Logic
- Probabilistic Transition Systems
- Stone Duality
- Coalgebraic Logic, Automata Theory, Fixed Point Logics
- Coalgebraic Logic for Structural Operational Semantics
- 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).
- Samson Abramsky (University of Oxford, GB) [dblp]
- Jiri Adamek (TU Braunschweig, DE)
- Ingo David Battenfeld (TU Dortmund, DE)
- Nick Bezhanishvili (Imperial College London, GB) [dblp]
- Marta Bilkova (Charles University - Prague, CZ)
- Marcello M. Bonsangue (Leiden University, NL) [dblp]
- Vincenzo Ciancia (University Complutense - Madrid, ES) [dblp]
- Corina Cirstea (University of Southampton, GB)
- Josée Desharnais (Université Laval - Québec, CA)
- Ernst-Erich Doberkat (TU Dortmund, DE)
- Fabio Gadducci (University of Pisa, IT) [dblp]
- Mai Gehrke (Radboud University Nijmegen, NL) [dblp]
- H. Peter Gumm (Universität Marburg, DE)
- Helle Hvid Hansen (TU Eindhoven, NL) [dblp]
- Bart Jacobs (Radboud University Nijmegen, NL) [dblp]
- Achim Jung (University of Birmingham, GB) [dblp]
- Klaus Keimel (TU Darmstadt, DE) [dblp]
- Christian Kissig (University of Leicester, GB)
- Bartek Klin (University of Cambridge, GB) [dblp]
- Clemens Kupke (Imperial College London, GB) [dblp]
- Alexander Kurz (University of Leicester, GB) [dblp]
- Raul Leal (University of Amsterdam, NL)
- Paul Blain Levy (University of Birmingham, GB) [dblp]
- Tadeusz Litak (University of Leicester, GB)
- Stefan Milius (TU Braunschweig, DE) [dblp]
- Lawrence S. Moss (Indiana University - Bloomington, US) [dblp]
- Alessandra Palmigiano (University of Amsterdam, NL) [dblp]
- Dirk Pattinson (Imperial College London, GB) [dblp]
- Dusko Pavlovic (University of Oxford, GB) [dblp]
- Daniela Petrisan (University of Leicester, GB) [dblp]
- Lutz Schröder (DFKI Bremen, DE)
- Christoph Schubert (TU Dortmund, DE)
- Ana Sokolova (Universität Salzburg, AT) [dblp]
- Sam Staton (University of Cambridge, GB) [dblp]
- Jiri Velebil (Czech Technical University, CZ)
- Yde Venema (University of Amsterdam, NL) [dblp]
- Jacob Vosmaer (University of Amsterdam, NL)
- Lijun Zhang (University of Oxford, GB) [dblp]
- Chunlai Zhou (Tsinghua University Beijing, CN)
- Dagstuhl Seminar 12411: Coalgebraic Logics (2012-10-07 - 2012-10-12) (Details)
- formal methods
- software engineering
- Modal logics
- bisimulation and behavioral equivalence
- Markov transition systems