Strong completeness for iteration-free coalgebraic dynamic logics

Clemens Kupke, Helle Hvid Hansen, Raul Andres Leal

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

6 Citations (Scopus)
90 Downloads (Pure)


We present a (co)algebraic treatment of iteration-free dynamic modal logics such as Propositional Dynamic Logic (PDL) and Game Logic (GL), both without star. The main observation is that the program/game constructs of PDL/GL arise from monad structure, and the axioms of these logics correspond to certain compatibilty requirements between the modalities and this monad structure. Our main contribution is a general soundness and strong completeness result for PDL-like logics for T-coalgebras where T is a monad and the "program" constructs are given by sequential composition, test, and pointwise extensions of operations of T.
Original languageEnglish
Title of host publicationTheoretical Computer Science
Subtitle of host publication8th IFIP TC 1/WG 2.2 International Conference, TCS 2014
EditorsJosep Diaz, Ivan Lanese, Davide Sangiorgi
Number of pages15
ISBN (Print)978-3-662-44601-0
Publication statusPublished - Sep 2014

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
ISSN (Print)0302-9743


  • propositional dynamic logic
  • game logic
  • strong completeness
  • coalgebraic dynamic modal logic


Dive into the research topics of 'Strong completeness for iteration-free coalgebraic dynamic logics'. Together they form a unique fingerprint.

Cite this