Formally Verifying a Transformation from MLTL Formulas to Regular Expressions

TL;DR

The paper presents a formally verified Isabelle/HOL formalization of the WEST algorithm that converts Mission-time Linear Temporal Logic (MLTL) formulas into logically equivalent trace regular expressions. It defines precise MLTL syntax and semantics, introduces trace and WEST regex representations, and proves core correctness lemmas for the core operators, temporal operators, and the top-level WEST algorithm, including a formally verified correctness theorem. A code export from the verified development generates a new WEST implementation used to validate existing unverified tools, and an auxiliary naïve equivalence checker provides trustworthy equivalence assessments. Experiments compare the verified Isabelle code against optimized WEST variants, showing competitive performance and enabling rigorous tool validation for safety-critical MLTL specifications. The work enhances trust in MLTL-based verification by delivering a fully verified pipeline from specification to regex-based analysis and opens avenues for extension to related logics and further verified tooling.

Abstract

Mission-time Linear Temporal Logic (MLTL), a widely used subset of popular specification logics like STL and MTL, is often used to model and verify real world systems in safety-critical contexts. As the results of formal verification are only as trustworthy as their input specifications, the WEST tool was created to facilitate writing MLTL specifications. Accordingly, it is vital to demonstrate that WEST itself works correctly. To that end, we verify the WEST algorithm, which converts MLTL formulas to (logically equivalent) regular expressions, in the theorem prover Isabelle/HOL. Our top-level result establishes the correctness of the regular expression transformation; we then generate a code export from our verified development and use this to experimentally validate the existing WEST tool. To facilitate this, we develop some verified support for checking the equivalence of two regular expressions.

Figures (10)

• Figure 1: For $\texttt{AP} = \{p_0, p_1\}$, the bit string of trace $\{p_0\}, \{p_0, p_1\}, \{\}, \{p_1\}$ is 10,11,00,01 (following the source material DBLP:conf/ifm/ElwingGSTWR23, we use commas to separate timesteps for readability) which is encoded in Isabelle as 1000 1000 1000 1000 1000 1000 [[1,0], [1, 1], [0, 0], [0, 1]] (type 1000 1000 1000 1000 1000 1000 nat list list).
• Figure 2: High-level overview of key components in our formalization of the WEST algorithm.
• Figure 3: Operations table for WEST_and operation for bits (left), and two examples of WEST_and between regex states and traces (middle and right).
• Figure 4: Two cactus plots, each comparing the three WEST implementations on $1000$ random formulas of varying nesting depth $d$, interval bounds $b$, and number of atomic propositions $n$. The number of total solved instances is shown on the y-axis, and the cumulative time taken is shown on the x-axis, with the number of timeouts labeled.
• Figure 5: Results for $n=5$, $b=2$, and varying values of $d$ from $0$ to $5$, with a batch size of 300 formulas per value of $d$. The Isabelle implementation is faster than the unoptimized WEST tool on most values of $d$, but times out on many formulas for $d=5$.