Talk "Linear Time Logics - A Coalgebraic Perspective"

by Corina Cirstea

Sat, 07 July 2018 at 10:10 am in Royal Holloway, United Kingdom

Abstract: We describe a principled approach to deriving linear time logics for a wide variety of state-based, quantitative models, by modelling the latter as coalgebras whose type incorporates both branching and linear behaviour. We define logics whose domain of truth values is determined by the choice of (quantitative) branching, and we provide two equivalent semantics for them: a path-based semantics akin to those of standard linear time logics, and a step-wise semantics that is more amenable to (automata-based) model checking. We also provide a semantic characterisation of the associated notion of logical equivalence. Instances of the logics support reasoning about the possibility, probability or minimal resources required to achieve a given linear time property. For resource-based models, a notion of offsetting can be used to model resource gain, thereby increases the practical appeal of the logics in the context of resource-aware computation.