Point algebras for temporal reasoning: Algorithms and complexity

We investigate the computational complexity of temporal reasoning in different time models such as totally-ordered, partially-ordered and branching time. Our main result concerns the satisfiability problem for point algebras and point algebras extended with disjunctions—for these problems, we identify all tractable subclasses. We also provide a number of additional results; for instance, we present a new time model suitable for reasoning about systems with a bounded number of unsynchronized clocks, we investigate connections with spatial reasoning and we present improved algorithms for deciding satisfiability of the tractable point algebras.