Deciding the Satisfiability of MITL Specifications

TL;DR

This paper introduces a new, practical decision procedure for MITL satisfiability by reducing it to a decidable logic, enabling the development of an effective SMT-based checking tool.

Contribution

It presents a satisfiability-preserving reduction from MITL to a decidable variant of CLTL, leading to a complete decision procedure and a prototype tool.

Findings

The reduction enables practical satisfiability checking for MITL.

A prototype SMT-based tool for MITL satisfiability has been implemented.

The approach outperforms automata-based methods in practicality.

Abstract

In this paper we present a satisfiability-preserving reduction from MITL interpreted over finitely-variable continuous behaviors to Constraint LTL over clocks, a variant of CLTL that is decidable, and for which an SMT-based bounded satisfiability checker is available. The result is a new complete and effective decision procedure for MITL. Although decision procedures for MITL 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 MITL based on the encoding presented here has, instead, been implemented and is publicly available.