Corina Cirstea - Linear-time logics -- a coalgebraic perspective

lmcs:8494 - Logical Methods in Computer Science, June 13, 2024, Volume 20, Issue 2 - https://doi.org/10.46298/lmcs-20(2:13)2024
Linear-time logics -- a coalgebraic perspectiveArticle

Authors: Corina Cirstea

    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.


    Volume: Volume 20, Issue 2
    Published on: June 13, 2024
    Accepted on: December 3, 2023
    Submitted on: September 17, 2021
    Keywords: Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 265 times.
    This article's PDF has been downloaded 114 times.