Picture of neon light reading 'Open'

Discover open research at Strathprints as part of International Open Access Week!

23-29 October 2017 is International Open Access Week. The Strathprints institutional repository is a digital archive of Open Access research outputs, all produced by University of Strathclyde researchers.

Explore recent world leading Open Access research content this Open Access Week from across Strathclyde's many research active faculties: Engineering, Science, Humanities, Arts & Social Sciences and Strathclyde Business School.

Explore all Strathclyde Open Access research outputs...

Strong completeness for iteration-free coalgebraic dynamic logics

Kupke, Clemens and Hansen, Helle Hvid and Leal, Raul Andres (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

[img]
Preview
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.