On the Satisfiability of Metric Temporal Logics over the Reals

We show that there is a satisfiability-preserving translation of QTL formulae interpreted over finitely variable behaviors into formulae of the CLTL-over-clocks logic. The satisfiability of CLTL-over-clocks can be determined through a suitable encoding into the input logics of SMT solvers, so it constitutes an effective decision procedure for QTL. Although decision procedures for determining satisfiability of QTL (and for the expressively equivalent logics MITL and QMLO) already exist, the automata-based techniques they employ appear to be very difficult to realize in practice, and, to the best of our knowledge, no implementation currently exists for them. A prototype tool for QTL based on the encoding presented here has, instead, been implemented and is publicly available.