Tractable Temporal Reasoning

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.