An automata-theoretic decision procedure for future interval logic

Abstract

Graphical Interval Logic (GIL) is a temporal logic in which all reasoning is done by means of diagrammatic formulae. It is a discrete linear-time modal logic in which the basic temporal modality is the interval. Future Interval Logic (FIL) provides the logical foundation for GIL. In this paper we present an automata-theoretic decision procedure for FIL with complexity DTIME(2O(nk)), where n is the size of the formula and k is the depth of interval nesting. For formulæ with bounded depth but length unbounded, the satisfiability problem for FIL is shown to be PSPACE-complete. We believe that this is the first result giving a direct decision procedure of elementary complexity for an interval logic. We also show that the logic is transparent to finite stuttering over the class of a-sequences, a feature that is useful for composition and refinement.