Search the Dagstuhl Website
Looking for information on the websites of the individual seminars? - Then please:
Not found what you are looking for? - Some of our services have separate websites, each with its own search option. Please check the following list:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Within this website:
External resources:
Within this website:
External resources:
  • the dblp Computer Science Bibliography

Dagstuhl Seminar 12411

Coalgebraic Logics

( Oct 07 – Oct 12, 2012 )

(Click in the middle of the image to enlarge)

Please use the following short url to reference this page:




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. Technically, the parameter F is a functor on a category C.

What has been achieved: The power of uniformity and modularity Following on from Moss' seminal paper, Coalgebraic Logic is now growing into a successful area. Conferences in this area now treat topics such as completeness, expressivity, compositionality, complexity, rule formats for process calculi, containing several hitherto unknown results on these classic topics.

The uniformity achieved in the above cited work is based on varying the type F for a given base category C, usually the category of sets. But it is also of interest to vary C.

Here probabilistic approaches deserve to be mentioned. In a number of papers Markov transition systems could be shown to interpret modal logics under different assumptions on the probabilistic structure. It was shown that general measurable spaces provide too general a structure, but that analytic spaces with Borel transition laws offer just the right blend of generality and measure theoretic accessibility. In this context, it was shown that logical equivalence, bisimilarity, and behavioral equivalence are equivalent concepts. Recent work shows that this can be extended to distributional aspects as well: instead of comparing states proper, one has a look at distributions over the states of a Kripke model. This approach was recently generalized from general modal logics to coalgebraic logics; these logics are interpreted through coalgebras in which the subprobability functor and the functor suggested by the phenomenon to be modelled form various syntactic alliances. This generalization brings stochastic coalgebraic logic into the mainstream of coalgebraic logics: the problems considered are similar, and one sees a convergence of methods.

Nevertheless it is to be mentioned that the probabilistic approach brings its own idiosyncratic touch due to measure theoretic problems. This entails among others that one sometimes has to work in a very specific topological context, for otherwise solutions are not available. On the other hand, leaving a topological context and working in general measurable spaces poses the question of the limits to the coalgebraic approach: What can be achieved in general measurable spaces, or in measurable spaces in which some of the properties are available (like Blackwell spaces, which are countably generated without being topological)?

Quantitative aspects are also considered when it comes to approximate Markov transition processes defined on uncountably infinite state spaces through finite processes. This is a classical problem that arises mostly in practical applications of Markov transition systems; it has to be investigated from a logical vantage point as well.

  • Samson Abramsky (University of Oxford, GB) [dblp]
  • Octavian Vladut Babus (University of Leicester, GB)
  • Jort Bergfeld (University of Amsterdam, NL)
  • Marta Bilkova (Charles University - Prague, CZ)
  • Marcello M. Bonsangue (Leiden University, NL) [dblp]
  • Liang-Ting Chen (University of Birmingham, GB)
  • Vincenzo Ciancia (CNR - Pisa, IT) [dblp]
  • Corina Cirstea (University of Southampton, GB)
  • Josée Desharnais (Université Laval - Québec, CA)
  • Ernst-Erich Doberkat (TU Dortmund, DE)
  • Matej Dostal (Czech Technical University, CZ)
  • Norman Francis Ferns (McGill University - Montreal, CA)
  • H. Peter Gumm (Universität Marburg, DE)
  • Helle Hvid Hansen (Radboud University Nijmegen, NL) [dblp]
  • Ichiro Hasuo (University of Tokyo, JP) [dblp]
  • Dirk Hofmann (University of Aveiro, PT)
  • Bart Jacobs (Radboud University Nijmegen, NL) [dblp]
  • Achim Jung (University of Birmingham, GB) [dblp]
  • Klaus Keimel (TU Darmstadt, DE) [dblp]
  • Dexter Kozen (Cornell University, US) [dblp]
  • Clemens Kupke (University of Oxford, GB) [dblp]
  • Alexander Kurz (University of Leicester, GB) [dblp]
  • Paul Blain Levy (University of Birmingham, GB) [dblp]
  • Tadeusz Litak (Universität Erlangen-Nürnberg, DE)
  • Stefan Milius (TU Braunschweig, DE) [dblp]
  • M. Andrew Moshier (Chapman University - Orange, US) [dblp]
  • Robert Myers (TU Braunschweig, DE) [dblp]
  • Alessandra Palmigiano (University of Amsterdam, NL) [dblp]
  • Prakash Panangaden (McGill University - Montreal, CA) [dblp]
  • Dusko Pavlovic (Royal Holloway University of London, GB) [dblp]
  • Daniela Petrisan (University of Leicester, GB) [dblp]
  • Katsuhiko Sano (JAIST - Ishikawa, JP) [dblp]
  • Lutz Schröder (Universität Erlangen-Nürnberg, DE) [dblp]
  • Alexandra Silva (Radboud University Nijmegen, NL) [dblp]
  • Ana Sokolova (Universität Salzburg, AT) [dblp]
  • Shashi M. Srivastava (Indian Statistical Institute - Kolkata, IN)
  • Sam Staton (University of Cambridge, GB) [dblp]
  • Pedro Sánchez Terraf (Universidad Nacional de Córdoba, AR)
  • Baltasar Trancon y Widemann (Universität Bayreuth, DE) [dblp]
  • Henning Urbat (TU Braunschweig, DE) [dblp]
  • Jiri Velebil (Czech Technical University, CZ)
  • Yde Venema (University of Amsterdam, NL) [dblp]
  • Joost Winter (CWI - Amsterdam, NL)
  • Chunlai Zhou (Renmin University of China - Beijing, CN)

Related Seminars
  • Dagstuhl Seminar 09502: Coalgebraic Logics (2009-12-06 - 2009-12-09) (Details)

  • semantcis/formal methods
  • verification/logic

  • Modal logics
  • coalgebras
  • bisimulation and behavioral equivalence
  • relations
  • Markov transition systems