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.
Type de document :
Communication dans un congrès
Josep Diaz; Ivan Lanese; Davide Sangiorgi. 8th IFIP International Conference on Theoretical Computer Science (TCS), Sep 2014, Rome, Italy. Springer, Lecture Notes in Computer Science, LNCS-8705, pp.281-295, 2014, Theoretical Computer Science. 〈10.1007/978-3-662-44602-7_22〉
Liste complète des métadonnées

Littérature citée [30 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01402072
Contributeur : Hal Ifip <>
Soumis le : jeudi 24 novembre 2016 - 11:05:57
Dernière modification le : jeudi 24 novembre 2016 - 11:14:10
Document(s) archivé(s) le : lundi 20 mars 2017 - 20:20:30

Fichier

978-3-662-44602-7_22_Chapter.p...
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Helle Hansen, Clemens Kupke, Raul Leal. Strong Completeness for Iteration-Free Coalgebraic Dynamic Logics. Josep Diaz; Ivan Lanese; Davide Sangiorgi. 8th IFIP International Conference on Theoretical Computer Science (TCS), Sep 2014, Rome, Italy. Springer, Lecture Notes in Computer Science, LNCS-8705, pp.281-295, 2014, Theoretical Computer Science. 〈10.1007/978-3-662-44602-7_22〉. 〈hal-01402072〉

Partager

Métriques

Consultations de la notice

20

Téléchargements de fichiers

7