Skip to Main content Skip to Navigation
Conference papers

Strong Completeness for Iteration-Free Coalgebraic Dynamic Logics

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [30 references]  Display  Hide  Download

https://hal.inria.fr/hal-01402072
Contributor : Hal Ifip <>
Submitted on : Thursday, November 24, 2016 - 11:05:57 AM
Last modification on : Wednesday, November 25, 2020 - 4:42:03 PM
Long-term archiving on: : Monday, March 20, 2017 - 8:20:30 PM

File

978-3-662-44602-7_22_Chapter.p...
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Helle Hansen, Clemens Kupke, Raul Leal. Strong Completeness for Iteration-Free Coalgebraic Dynamic Logics. 8th IFIP International Conference on Theoretical Computer Science (TCS), Sep 2014, Rome, Italy. pp.281-295, ⟨10.1007/978-3-662-44602-7_22⟩. ⟨hal-01402072⟩

Share

Metrics

Record views

87

Files downloads

624