线性时间逻辑 -- 一种共代数观点
摘要：从范畴中一种模型的分支行为和线性行为来推导出一种广泛适用于基于状态的定量系统的线性时间逻辑的一般方法。具体来说，我们定义了一种逻辑，其语法由线性行为的类型决定，真值域由分支行为的类型决定，并提供了两种语义：类似于标准范畴逻辑的逐步语义和类似于标准线性时间逻辑的路径语义。前者适用于模型检验，而后者是更自然的语义，因为它衡量了给定状态的计算路径上的定性属性的持续程度。我们的主要结果是这两种语义的等价性。我们还提供了一种由这些逻辑引出的逻辑距离的语义刻画。我们的逻辑实例支持关于展示给定线性时间属性的可能性、可能性或最小成本的推理。
作者：Corina Cirstea
论文ID：1612.07844
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-07-13