Deciding Continuous-Time Metric Temporal Logic with Counting Modalities

We present a satisfiability-preserving translation of QTL formulae with counting modalities interpreted over finitely variable signals into formulae of the CLTL-over-clocks logic. The satisfiability of CLTL-over-clocks can be solved through a suitable encoding into the input logics of SMT solvers, so our translation constitutes an effective decision procedure for QTL with counting modalities. It is known that counting modalities increase the expressiveness of QTL (hence also of the expressively equivalent MITL logic); to the best of our knowledge, our decision procedure for such modalities is the first actually implemented.