Interval vs. Point Temporal Logic Model Checking

doi:10.1145/3281028

Interval vs. Point Temporal Logic Model Checking

2018-12-20

0

OA

AI

DOI：10.1145/3281028

原文链接

查看原文

摘要

En 中文

近年来，基于区间时态逻辑的模型检测正作为一种可行的替代方案，与基于标准点式时态逻辑（如LTL、CTL、CTL*等）的模型检测相竞争。系统的行为通常通过（有限）Kripke结构进行建模。然而，虽然“点式”解释的时态逻辑描述系统如何逐状态演化并谓词化系统状态的属性，但“区间式”解释的时态逻辑则表达跨越一系列状态的计算区间的属性。假设一个命题字母在一个计算区间（区间）上成立，当且仅当它在每个组成状态上成立（均一性假设）。一个自然的问题是：将基本时间实体从点替换为区间是否有任何优势，或者这仅仅是个偏好问题？本文研究Halpern和Shoham的区间时态逻辑（HS）在模型检测中的表达能力，并将其与LTL、CTL和CTL*进行比较。为此，我们考虑HS的三种语义变体：由Montanari等人[30, 34]引入的状态基变体，允许时间在现在和未来均分支；计算树基变体，仅允许时间在未来分支；以及轨迹基变体，禁止时间分支。这些变体相互之间以及与上述标准逻辑进行比较，以获得完整的图景。具体而言，我们证明：轨迹基语义的HS等价于LTL（但至少指数级更简洁），计算树基语义的HS等价于有限CTL*，而状态基语义的HS与它们（LTL、CTL和CTL*）均不可比较。

Interval vs. Point Temporal Logic Model Checking

摘要

AI总结

期刊

机构

引用论文