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.

翻译：我们描述了一种通用方法，可用于推导面向多种基于状态的定量系统的线性时态逻辑，其核心思路是将这些系统建模为兼具分支行为与线性行为类型的余代数。具体而言，我们定义了逻辑：其语法由线性行为类型决定，其真值域由分支行为类型决定，并为它们提供了两种语义：一种类似于标准余代数逻辑的逐步语义，另一种类似于标准线性时态逻辑的基于路径的语义。前者语义适用于模型检验，而后者语义更为自然，因为它度量了从给定状态出发的计算路径上定性性质的满足程度。本文主要结果证明了这两种语义的等价性。我们还对这些逻辑所诱导的逻辑距离概念给出了语义刻画。本文逻辑的实例支持对呈现给定线性时态性质的可能性、似然性或最小代价进行推理。