Picture of automobile manufacturing plant

Driving innovations in manufacturing: Open Access research from DMEM

Strathprints makes available Open Access scholarly outputs by Strathclyde's Department of Design, Manufacture & Engineering Management (DMEM).

Centred on the vision of 'Delivering Total Engineering', DMEM is a centre for excellence in the processes, systems and technologies needed to support and enable engineering from concept to remanufacture. From user-centred design to sustainable design, from manufacturing operations to remanufacturing, from advanced materials research to systems engineering.

Explore Open Access research by DMEM...

Weak completeness of coalgebraic dynamic logics

Hansen, Helle Hvid and Kupke, Clemens (2015) Weak completeness of coalgebraic dynamic logics. In: Proceedings Tenth International Workshop on Fixed Points in Computer Science. Electronic Proceedings in Theoretical Computer Science, Berlin, pp. 90-104.

[img]
Preview
Text (Hansen-Kupke-FICS-2015-Weak-completeness-of-coalgebraic-dynamic)
Hansen_Kupke_FICS_2015_Weak_completeness_of_coalgebraic_dynamic.pdf - Final Published Version
License: Creative Commons Attribution 3.0 logo

Download (175kB) | Preview

Abstract

We present a coalgebraic generalisation of Fischer and Ladner's Propositional Dynamic Logic (PDL) and Parikh's Game Logic (GL). In earlier work, we proved a generic strong completeness result for coalgebraic dynamic logics without iteration. The coalgebraic semantics of such programs is given by a monad T, and modalities are interpreted via a predicate lifting \^I whose transpose is a monad morphism from T to the neighbourhood monad. In this paper, we show that if the monad T carries a complete semilattice structure, then we can define an iteration construct, and suitable notions of diamond-likeness and box-likeness of predicate-liftings which allows for the definition of an axiomatisation parametric in T, \^I and a chosen set of pointwise program operations. As our main result, we show that if the pointwise operations are "negation-free" and Kleisli composition left-distributes over the induced join on Kleisli arrows, then this axiomatisation is weakly complete with respect to the class of standard models. As special instances, we recover the weak completeness of PDL and of dual-free Game Logic. As a modest new result we obtain completeness for dual-free GL extended with intersection (demonic choice) of games.