A tool for deciding the satisfiability of continuous-time metric temporal logic

Constraint LTL over clocks is a variant of CLTL, an extension of linear-time temporal logic allowing atomic assertions in a concrete constraint system. Satisfiability of CLTL over clocks is here shown to be decidable by means of a reduction to a decidable Satisfiability Modulo Theories (SMT) problem. The result is a complete Bounded Satisfiability Checking procedure, which has been implemented by using standard SMT solvers. The importance of this technique derives from the possibility of translating various continuous-time metric temporal logics, such as MITL and QTL, into CLTL over clocks itself. Although standard decision procedures of these logics do exist, they have never been realized in practice. Suitable translations into CLTL over clocks have instead allowed us the development of the first prototype tool for deciding MITL and QTL. The paper also reports preliminary, but encouraging, experiments on some significant examples of MITL and QTL formulae.