You can manage bookmarks using lists, please log in to your user account for this.
Media type:
E-Article
Title:
Linear-time logics -- a coalgebraic perspective
Contributor:
Cirstea, Corina
Published:
Centre pour la Communication Scientifique Directe (CCSD), 2024
Published in:
Logical Methods in Computer Science, Volume 20, Issue 2 (2024)
Language:
English
DOI:
10.46298/lmcs-20(2:13)2024
ISSN:
1860-5974
Origination:
Footnote:
Description:
We describe a general approach to deriving linear-time logics for a widevariety of state-based, quantitative systems, by modelling the latter ascoalgebras whose type incorporates both branching and linear behaviour.Concretely, we define logics whose syntax is determined by the type of linearbehaviour, and whose domain of truth values is determined by the type ofbranching behaviour, and we provide two semantics for them: a step-wisesemantics akin to that of standard coalgebraic logics, and a path-basedsemantics akin to that of standard linear-time logics. The former semantics isuseful for model checking, whereas the latter is the more natural semantics, asit measures the extent with which qualitative properties hold along computationpaths from a given state. Our main result is the equivalence of the twosemantics. We also provide a semantic characterisation of a notion of logicaldistance induced by these logics. Instances of our logics support reasoningabout the possibility, likelihood or minimal cost of exhibiting a givenlinear-time property.