Tractable Temporal Reasoning
Tractable Temporal Reasoning
复制标题
DOI：
--
复制
发表时间：
2007-01
期刊：
影响因子：
--
通讯作者：
C. Dixon;Michael Fisher;B. Konev
中科院分区：
文献类型：
--
作者：
C. Dixon;Michael Fisher;B. Konev
时间推理在计算机科学和人工智能领域都有广泛的应用。然而，离散时态逻辑中时态证明的潜在复杂性导致了使用简化的形式主义和技术，例如时态区间代数或模型检查。在本文中，我们表明，听话的子类命题线性时序逻辑可以开发，使用XOR片段的逻辑。我们不仅表明，这样的片段可以决定，可追溯的，通过子句的时间分辨率，但也显示了多个XOR片段相结合的好处。对于这样的组合，我们建立的完整性和复杂性（决议的方法），并描述了这样一个时间的语言可能会被用于应用领域，例如多代理系统的验证。这种新的时间推理方法提供了一个框架，在这个框架中，可以通过智能地组合适当的XOR片段来设计易处理的时间逻辑。
Temporal reasoning is widely used within both Computer Science and A.I. However, the underlying complexity of temporal proof in discrete temporal logics has led to the use of simplified formalisms and techniques, such as temporal interval algebras or model checking. In this paper we show that tractable sub-classes of propositional linear temporal logic can be developed, based on the use of XOR fragments of the logic. We not only show that such fragments can be decided, tractably, via clausal temporal resolution, but also show the benefits of combining multiple XOR fragments. For such combinations we establish completeness and complexity (of the resolution method), and also describe how such a temporal language might be used in application areas, for example the verification of multi-agent systems. This new approach to temporal reasoning provides a framework in which tractable temporal logics can be engineered by intelligently combining appropriate XOR fragments.