一句话：证明同质性假设下子区间逻辑 D 的有限可满足性与模型检测均为 PSPACE 完全，拓展了易处理区间时序逻辑。
区间时序逻辑表达力强，但因复杂度高长期难以用于实际。本文研究仅含子区间关系模态的逻辑 D，在同质性假设（命题字母在区间上成立当且仅当其在区间内所有点成立）下的有限可满足性与模型检测。作者分别在有限线性序和有限 Kripke 结构上分析这两个问题，证明可满足性问题是 PSPACE 完全的，并进一步证明模型检测问题同样 PSPACE 完全。该结果将 D 纳入计算上易处理的区间时序逻辑之列，为规范、验证与规划等应用提供了新的可判定且复杂度可控的逻辑基础。
The expressive power of interval temporal logics (ITLs) makes them one of the most natural choices in a number of application domains, ranging from the specification and verification of complex reactive systems to automated planning. However, for a long time, because of their high computational complexity, they were considered not suitable for practical purposes. The recent discovery of several computationally well-behaved ITLs has finally changed the scenario. In this paper, we investigate the finite satisfiability and model checking problems for the ITL D, that has a single modality for the sub-interval relation, under the homogeneity assumption (that constrains a proposition letter to hold over an interval if and only if it holds over all its points). We first prove that the satisfiability problem for D, over finite linear orders, is PSPACE-complete, and then we show that the same holds for its model checking problem, over finite Kripke structures. In such a way, we enrich the set of tractable interval temporal logics with a new meaningful representative.
@article{paperbot1732,
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 = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 1},
year = {2022},
doi = {10.46298/lmcs-18(1:24)2022}
}