%0 Conference Proceedings
%T Strong Completeness for Iteration-Free Coalgebraic Dynamic Logics
%+ Radboud University [Nijmegen]
%+ Centrum Wiskunde & Informatica (CWI)
%+ University of Strathclyde [Glasgow]
%+ Cap Gemini [Amsterdam]
%A Hansen, Helle, Hvid
%A Kupke, Clemens
%A Leal, Raul, Andres
%Z Part 2: Track B: Logic, Semantics, Specification and Verification
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 8th IFIP International Conference on Theoretical Computer Science (TCS)
%C Rome, Italy
%Y Josep Diaz
%Y Ivan Lanese
%Y Davide Sangiorgi
%I Springer
%3 Theoretical Computer Science
%V LNCS-8705
%P 281-295
%8 2014-09-01
%D 2014
%R 10.1007/978-3-662-44602-7_22
%Z Computer Science [cs]Conference papers
%X 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.
%G English
%Z TC 1
%Z TC 2
%Z WG 2.2
%2 https://inria.hal.science/hal-01402072/document
%2 https://inria.hal.science/hal-01402072/file/978-3-662-44602-7_22_Chapter.pdf
%L hal-01402072
%U https://inria.hal.science/hal-01402072
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-TC2
%~ IFIP-LNCS-8705
%~ IFIP-TCS
%~ IFIP-WG2-2