Picture of athlete cycling

Open Access research with a real impact on health...

The Strathprints institutional repository is a digital archive of University of Strathclyde's Open Access research outputs. Strathprints provides access to thousands of Open Access research papers by Strathclyde researchers, including by researchers from the Physical Activity for Health Group based within the School of Psychological Sciences & Health. Research here seeks to better understand how and why physical activity improves health, gain a better understanding of the amount, intensity, and type of physical activity needed for health benefits, and evaluate the effect of interventions to promote physical activity.

Explore open research content by Physical Activity for Health...

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

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


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.