Linear-time logics -- a coalgebraic perspective
Corina Cirstea
TL;DR
This work develops a unifying coalgebraic framework for linear-time logics over quantitative state-based systems by modelling systems as ${\mathsf T}_S \circ F$-coalgebras, where $F$ captures linear behaviour and ${\mathsf T}_S$ encodes branching via a partial semiring $S$. It introduces both step-wise and path-based semantics for the induced logics and proves their equivalence, enabling both model checking and pathwise reasoning in a single semantic setting. A theory of ${\mathsf S}$-valued measures on σ-algebras is developed to support semiring-valued path semantics and a semantic notion of linear-time distance between states is defined, shown to coincide with a logical distance induced by the logics. The resulting quantitative linear-time fixpoint logics, instantiated to various semirings (e.g., boolean, probabilistic, tropical), subsume existing LTL-like logics for non-deterministic and probabilistic systems while generalising to resource-aware and tree-shaped branching models; equi-expressiveness with standard linear-time automata is established via automata-theoretic translations. Overall, the framework enables uniform reasoning about possibility, likelihood, and cost of linear-time properties across a broad class of branching systems, with solid theoretical guarantees linking two natural semantics and a robust notion of distance.
Abstract
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 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. The former semantics is useful for model checking, whereas the latter is the more natural semantics, as it measures the extent with which qualitative properties hold along computation paths from a given state. Our main result is the equivalence of the two semantics. 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.