MightyPPL: Verification of MITL with Past and Pnueli Modalities

TL;DR

This work tackles the expressiveness gap of MITL by introducing MITPPL, an extension that adds Past and Pnueli modalities. MightyPPL provides a fully compositional translation from MITPPL to standard timed automata via tester automata, enabling satisfiability and model checking against multiple back-ends for both finite and infinite words. Key innovations include a bounded abstraction for general intervals, a sequentialisation technique to control state space growth, and a symbolic encoding of transitions to improve efficiency. The implementation demonstrates substantial performance gains across diverse benchmarks (including real-time CPS scenarios) and maintains broad back-end compatibility, highlighting the approach's practical impact for expressive real-time specification verification.

Abstract

Metric Interval Temporal Logic (MITL) is a popular formalism for specifying properties of reactive systems with timing constraints. Existing approaches to using MITL in verification tasks, however, have notable drawbacks: they either support only limited fragments of the logic or allow for only incomplete verification. This paper introduces MightyPPL, a new tool for translating formulae in Metric Interval Temporal Logic with Past and Pnueli modalities (MITPPL) over the pointwise semantics into timed automata. MightyPPL enables satisfiability and model checking of a much more expressive specification logic over both finite and infinite words and incorporates a number of performance optimisations, including a novel symbolic encoding of transitions and a symmetry reduction technique that leads to an exponential improvement in the number of reachable discrete states. For a given MITPPL formula, MightyPPL can generate either a network of timed automata or a single timed automaton that is language-equivalent and compatible with multiple verification back-ends, including Uppaal, TChecker, and LTSmin, which supports multi-core model checking. We evaluate the performance of the toolchain across various case studies and configuration options.

Figures (22)

• Figure 1: City map with eateries and other locations. Icons denote eateries (, , ), driver's initial location (), and customer locations (). Edges represent shortest travel times.
• Figure 2: A $\mathsf{TA}$ with finite-word acceptance condition (above) and the corresponding 'reverse' $\mathsf{TA}$ (below). The $\mathsf{TA}$ above has a single clock $x$ and four transitions (numbered $1$ to $4$ from left to right), thus we have the clocks $x_i^u, x_i^{\ell}$ for $1 \leq i \leq 4$ and each location has a bit-vector of length $4$.
• Figure 3: The finite-word tester $\mathsf{TA}$ for $\phi_1\mathbin{\mathbf{{U}}}_{\geq l} \phi_2$.
• Figure 4: The tester $\mathsf{TA}$ for $\phi_1\mathbin{\mathbf{{S}}}_{\geq l} \phi_2$.
• Figure 5: A component $\mathsf{TA}$ of the finite-word tester $\mathsf{TA}$ for $\mathop{\mathrm{\mathbf{P \mkern-2mu n}}}\nolimits_{< u}(\phi_1, \phi_2, \phi_3, \phi_4)$.

Theorems & Definitions (37)

• Example 1: Adapted from concur25
• Remark 1
• Example 2
• Remark 2
• Lemma 1
• proof
• Remark 3
• Example 3
• Lemma 2
• proof