Linear Time Logics -- A Coalgebraic Perspective

We describe a general approach to deriving linear-time logics for a wide variety of state-based, quantitative systems, by modelling the latter as coalgebras whose type incorporates both branching and linear behaviour. Concretely, we define logics whose syntax is determined by the type of linear behaviour, and whose domain of truth values is determined by the type of branching behaviour, and we provide two equivalent semantics for them: a step-wise semantics akin to that of standard coalgebraic logics, and a path-based semantics akin to that of standard linear-time logics. We also provide a semantic characterisation of a notion of logical distance induced by these logics. Instances of our logics support reasoning about the possibility, likelihood or minimal cost of exhibiting a given linear-time property.