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)
87 Downloads (Pure)

Abstract

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
PublisherSpringer
Pages281-295
Number of pages15
Volume8705
ISBN (Print)978-3-662-44601-0
DOIs
Publication statusPublished - Sep 2014

Publication series

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

    Fingerprint

Keywords

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

Cite this

Kupke, C., Hansen, H. H., & Leal, R. A. (2014). Strong completeness for iteration-free coalgebraic dynamic logics. In J. Diaz, I. Lanese, & D. Sangiorgi (Eds.), Theoretical Computer Science: 8th IFIP TC 1/WG 2.2 International Conference, TCS 2014 (Vol. 8705, pp. 281-295). (Lecture Notes in Computer Science; Vol. 8705). Springer. https://doi.org/10.1007/978-3-662-44602-7_22