基于轨迹代表的Halpern与Shoham区间时序逻辑片段的模型检测
计算机科学中的逻辑
2019-02-07 v1
摘要
模型检测允许针对系统行为的形式化模型（通常为 Kripke 结构）自动验证其预期属性的规范。基于点的时序逻辑，如 LTL、CTL 和 CTL*，描述系统如何逐状态演化，常被用作规范语言。它们在多种应用领域被证明相当成功。然而，约束时间扩展事件的时间顺序的属性以及涉及时间聚合的属性（本质上是基于区间的）无法被它们妥善处理。区间时序逻辑（ITLs）以区间为基本时间实体，被证明非常适合计算和区间属性的规范与验证（我们将 Kripke 结构的所有轨迹解释为计算区间）。我们研究 Halpern 与 Shoham 区间模态逻辑（HS）某些片段的模型检测问题。HS 为区间对之间每种可能的排序关系（即所谓的 Allen 关系）提供一种模态。首先，我们描述了针对 Allen 关系 meets、met-by、starts、started-by 和 finishes 的 HS 片段的 EXPSPACE 模型检测算法，该算法利用了为每条轨迹（长度无界）寻找等效有界长度轨迹代表的可能性。在检测属性时，只需考虑长度不超过给定界的轨迹。我们证明了该片段的模型检测问题是 PSPACE 困难的。最后，我们确定了其他行为良好的 HS 片段，它们表达力足够捕获系统的有意义区间属性，如互斥、状态可达性和无饥饿，且其复杂度小于或等于 LTL 的复杂度。
引用
@article{arxiv.1709.01849,
title = {Model Checking for Fragments of Halpern and Shoham's Interval Temporal Logic Based on Track Representatives},
author = {Alberto Molinari and Angelo Montanari and Adriano Peron},
journal= {arXiv preprint arXiv:1709.01849},
year = {2019}
}