MightyPPL: Model Checking MITL with Past and Pnueli Modalities

Abstract

Metric Interval Temporal Logic ( $$\textsf {MITL} $$ ) is a popular formalism for specifying properties of reactive systems with timing constraints. Existing approaches to using $$\textsf {MITL} $$ in verification tasks, however, have notable drawbacks: they either support only limited fragments of the logic (the future only fragment $$\textsf {MITL} [\textsf{Fut}]$$ ) or allow for only incomplete verification. This paper introduces $$\textsc {MightyPPL} $$ , a new tool for translating formulae in Metric Interval Temporal Logic with Past and Pnueli modalities ( $$\textsf {MITPPL} $$ ) over the pointwise semantics into timed automata, enabling satisfiability and model checking of this expressive specification logic over both finite and infinite timed words. $$\textsc {MightyPPL} $$ optimises performance via specialised constructions for simple cases, a novel symbolic transition encoding, and a symmetry reduction technique that yields an exponential improvement in reachable discrete states. The tool generates language-equivalent automata compatible with back-ends such as Uppaal, TChecker, and LTSmin. Our evaluation demonstrates that $$\textsc {MightyPPL} $$ significantly outperforms the state-of-the-art tool $$\textsc {MightyL} $$ on future-only fragments and across various benchmarks.