一句话：用余代数统一构造线性时间逻辑，并证明逐步语义与路径语义等价。
本文提出一种从余代数视角统一推导线性时间逻辑的一般方法，面向广泛的状态基定量系统。作者将系统建模为一种余代数，其类型同时编码分支行为与线性行为；逻辑的语法由线性行为类型决定，真值域由分支行为类型决定。论文给出两种语义：类似标准余代数逻辑的逐步语义，以及类似标准线性时间逻辑的路径语义，前者便于模型检测，后者更自然地度量给定状态沿计算路径满足定性属性的程度。主要结果是两种语义的等价，并对由这些逻辑诱导的逻辑距离给出语义刻画。实例表明该框架可推理线性时间属性的可能性、似然或最小代价。
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.