Strong completeness for iteration-free coalgebraic dynamic logics
Kupke, Clemens and Hansen, Helle Hvid and Leal, Raul Andres; Diaz, Josep and Lanese, Ivan and Sangiorgi, Davide, eds. (2014) Strong completeness for iteration-free coalgebraic dynamic logics. In: Theoretical Computer Science. Lecture Notes in Computer Science, 8705 . Springer, pp. 281-295. ISBN 978-3-662-44601-0
![]()
|
PDF (Hansen-etal-TCS2014-strong-completeness-for-iteration-free-coalgebraic-dynamic-logics)
Hansen_etal_TCS2014_strong_completeness_for_iteration_free_coalgebraic_dynamic_logics.pdf Accepted Author Manuscript Download (412kB)| Preview |
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.
Creators(s): | Kupke, Clemens, Hansen, Helle Hvid and Leal, Raul Andres; Diaz, Josep, Lanese, Ivan and Sangiorgi, Davide | Item type: | Book Section |
---|---|
ID code: | 51156 |
Notes: | The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-662-44602-7_22 |
Keywords: | propositional dynamic logic, game logic, strong completeness, coalgebraic dynamic modal logic, Mathematics, Computational Theory and Mathematics |
Subjects: | Science > Mathematics |
Department: | Faculty of Science > Computer and Information Sciences |
Depositing user: | Pure Administrator |
Date deposited: | 19 Jan 2015 12:22 |
Last modified: | 01 Jan 2021 06:50 |
Related URLs: | |
URI: | https://strathprints.strath.ac.uk/id/eprint/51156 |
Export data: |