论文标题
在同质性假设下的逻辑上的满意度和模型检查
Satisfiability and Model Checking for the Logic of Sub-Intervals under the Homogeneity Assumption
论文作者
论文摘要
间隔时间逻辑（ITL）的表达能力使它们成为许多应用程序域中最自然的选择之一，范围从复杂的反应系统的规范和验证到自动化计划。但是，由于它们的计算复杂性很高，因此很长一段时间以来，它们被认为不适合实际目的。最近发现的几个计算行为良好的ITL的发现终于改变了情景。 在本文中，我们研究了ITL D的有限满足和模型检查问题，该问题在同质性假设下具有单一的模式，该模态对亚间隔关系具有单一的模式（该命题字母限制了一个命题信以在且仅在所有点上占据时才在一个间隔上保留）。我们首先证明D在有限的线性订单上的满足性问题是PSPACE填充，然后我们证明其模型检查问题相同，而不是有限的Kripke结构。通过这种方式，我们通过新的有意义的代表来丰富一组可拖动的间隔时间逻辑。
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.
