A Tool that Incrementally Approximates Finite Satisfiability in Full Interval Temporal Logic?

Abstract. Interval Temporal Logic (ITL) is a powerful formalism to reason about sequences of events that can occur simultaneously and in an overlapping fashion. Despite its importance for various application domains, little tool support for au-tomated ITL reasoning is available, possibly also owed to ITL’s undecidability. We consider bounded satisfiability which approximates finite satisfiability and is only NP-complete. We provide an encoding into SAT that is designed to use the power of modern incremental SAT solvers. We present a tool that tests an ITL specification for finite satisfiability.