Efficient Verification of Metric Temporal Properties with Past in Pointwise Semantics

TL;DR

The paper addresses efficient verification of MITL in pointwise semantics by translating the past fragment to synchronous networks of deterministic timed automata ($\mathsf{det}\mathsf{MITL}^{+p}$) and extending to full MITL via generalized timed automata with future clocks. It introduces a two-stage translation framework, advances liveness analysis with an SCC-based approach for GTA, and implements Tempora, which significantly outperforms the state-of-the-art MightyL on satisfiability benchmarks and supports end-to-end model checking on standard benchmarks like Fischer's mutual exclusion and Dining Philosophers. The key contributions include linear-time past-to-TA translation, a scalable GTA-based framework for future modalities, novel two-state Until construction leveraging non-Zenoness, and engineering optimizations (prediction sharing, specialized F automata, memory reuse) that yield substantial practical speedups. Together, these advances enable robust, scalable verification of rich MITL^{+p} properties in real-time systems under pointwise semantics, with strong empirical support supporting broader adoption in verification workflows.

Abstract

Model checking for real-timed systems is a rich and diverse topic. Among the different logics considered, Metric Interval Temporal Logic (MITL) is a powerful and commonly used logic, which can succinctly encode many interesting timed properties especially when past and future modalities are used together. In this work, we develop a new approach for MITL model checking in the pointwise semantics, where our focus is on integrating past and maximizing determinism in the translated automata. Towards this goal, we define synchronous networks of timed automata with shared variables and show that the past fragment of MITL can be translated in linear time to synchronous networks of deterministic timed automata. Moreover determinism can be preserved even when the logic is extended with future modalities at the top-level of the formula. We further extend this approach to the full MITL with past, translating it into networks of generalized timed automata (GTA) with future clocks (which extend timed automata and event clock automata). We present an SCC-based liveness algorithm to analyse GTA. We implement our translation in a prototype tool which handles both finite and infinite timed words and supports past modalities. Our experimental evaluation demonstrates that our approach significantly outperforms the state-of-the-art in MITL satisfiability checking in pointwise semantics on a benchmark suite of 72 formulas. Finally, we implement an end-to-end model checking algorithm for pointwise semantics and demonstrate its effectiveness on two well-known benchmarks.

Figures (12)

• Figure 1: Synchronous Network of timed automata with shared variables. The model $\mathcal{M}$ is not drawn and owns the boolean variables $\mathsf{Prop}=\{p,q,r\}$. To lighten the figures above, we simply write $p^{\bullet}$, $q^{\bullet}$ and $r^{\bullet}$ instead of ${\mathcal{M}}.p^{\bullet}$, ${\mathcal{M}}.q^{\bullet}$ and ${\mathcal{M}}.r^{\bullet}$. The automata $\mathcal{A}_1$, $\mathcal{A}_2$, $\mathcal{A}_3$ own respectively the clock variables $x$, $y$ and $z$. The names and initial conditions are depicted with an incoming arrow to a location. For instance, the initial condition of $\mathcal{A}_2$ is $\mathsf{st}=\ell_{0}\wedge y=+\infty$. Notice that $\mathcal{A}_3$ refers to the post values of the state ${\mathcal{A}_2}.\mathsf{st}^{\bullet}$ and clock ${\mathcal{A}_2}.y^{\bullet}$ of $\mathcal{A}_2$.
• Figure 2: Automaton $\mathcal{A}^{isat}_{p}$.
• Figure 3: Left: Clock $x_{\sf{init}}$ is reset on the first event and measures time elapsed for all the initial satisfiability automata ($\mathcal{A}^{isat}_{\mathop{\mathsf{X}\newline}\nolimits_I}$ and $\mathcal{A}^{isat}_{\mathbin{\mathsf{U}}_I}$). Right: Automaton $\mathcal{A}^{isat}_{\mathop{\mathsf{X}\newline}\nolimits_I}$ for initial satisfiability for $\mathop{\mathsf{X}\newline}\nolimits_{I}b_1$. The boolean variable $b_1$ is not owned by $\mathcal{A}^{isat}_{\mathop{\mathsf{X}\newline}\nolimits_I}$ and stands for the argument of $\mathop{\mathsf{X}\newline}\nolimits_I$. In $\mathcal{A}^{isat}_{\mathop{\mathsf{X}\newline}\nolimits_I}$, we simply write $x_{\sf{init}}$ instead of ${\mathcal{A}_{\sf{init}}}.{x_{\sf{init}}}$. The automaton is deterministic and complete. If a run reaches state 3 (resp. 4) then $\mathop{\mathsf{X}\newline}\nolimits_{I}b_1$ was initially true (resp. false).
• Figure 4: Automaton $\mathcal{A}^{isat}_{\mathbin{\mathsf{U}}_I}$ for the initial satisfiability for $b_1 \mathbin{\mathsf{U}}_{I} b_2$ (with $I\neq\emptyset$). The boolean variables $b_1,b_2$ are not owned by $\mathcal{A}^{isat}_{\mathbin{\mathsf{U}}_I}$ and stand for the left and right arguments of $\mathbin{\mathsf{U}}_I$. The automaton is deterministic and complete. We write $x_{\sf{init}}<I$ (resp. $x_{\sf{init}}>I$) to state that $x_{\sf{init}}$ is smaller (resp. larger) than all values in $I$. For instance, if $I=[b,c)$ with $b<c$ then $x_{\sf{init}}<I$ means $x_{\sf{init}}<b$ and $x_{\sf{init}}>I$ means $x_{\sf{init}}\geq c$. If a run reaches state 2 (resp. 3) then we know for sure that $b_1 \mathbin{\mathsf{U}}_{I} b_2$ was initially true (resp. false). State 1 means we still do not know whether $b_1 \mathbin{\mathsf{U}}_{I} b_2$ was initially true. If the run stays forever in state 1, $b_1 \mathbin{\mathsf{U}}_{I} b_2$ was initially false.
• Figure 5: Left: Automaton $\mathcal{A}_{\mathop{\mathsf{Y}\newline}\nolimits}$ for the untimed Yesterday operator $\mathop{\mathsf{Y}\newline}\nolimits b_1$. The boolean variable $b_1$ is not owned by $\mathcal{A}_{\mathop{\mathsf{Y}\newline}\nolimits}$ and stands for the argument of $\mathop{\mathsf{Y}\newline}\nolimits$. Right: Sharer automaton $\mathcal{A}_{\sf{last}}$ with clock $x_{\sf{last}}$ used by all Yesterday operators.

Theorems & Definitions (26)

• Definition 1: Timed automaton with shared variables
• Definition 2: Synchronous network of timed automata
• Example 3
• Definition 4: $\mathsf{det}\sf{MITL}^{+p}$
• Theorem 5
• Lemma 5
• Lemma 5
• Lemma 6
• Lemma 6
• Lemma 6