齐性假设下子区间逻辑的可满足性与模型检测
计算机科学中的逻辑
2023-06-22 v3 形式语言与自动机理论
摘要
区间时序逻辑（ITLs）的表达能力使其成为众多应用领域中最自然的选择之一，范围从复杂反应系统的规约与验证到自动规划。然而，长期以来，由于其高计算复杂度，它们被认为不适合实际用途。近期若干计算上良行为的 ITLs 的发现最终改变了这一局面。本文中，我们在齐性假设（约束命题字母在一个区间上成立当且仅当其所有点上均成立）下，研究具有单一子区间关系模态的 ITL D 的有限可满足性与模型检测问题。我们首先证明 D 在有限线性序上的可满足性问题是 PSPACE 完全的，随后表明其在有限 Kripke 结构上的模型检测问题同为 PSPACE 完全。由此，我们以一个新的有意义代表丰富了可处理区间时序逻辑的集合。
引用
@article{arxiv.2006.04652,
title = {Satisfiability and Model Checking for the Logic of Sub-Intervals under the Homogeneity Assumption},
author = {Laura Bozzelli and Alberto Molinari and Angelo Montanari and Adriano Peron and Pietro Sala},
journal= {arXiv preprint arXiv:2006.04652},
year = {2023}
}
备注
arXiv admin note: text overlap with arXiv:1901.03880