Simplifying LTL Model Checking Given Prior Knowledge

TL;DR

This work tackles improving LTL model checking by exploiting prior knowledge K that over-approximates the system behavior (L(S) ⊆ L(K)). It introduces automata-based techniques that replace the negated property automaton A_{¬φ} with a simpler B derived from K, using language bounds, product/sum constructions, and transition-level Boolean bounds, including Minato's bound refinement. It further extends to stutter-insensitive automata and incremental knowledge integration, enabling cheaper, progressive simplifications across multiple knowledge facts. Empirical evaluation on MCC'22 shows that a large portion of problems can be answered without full model checking and that the remaining cases benefit substantially from the proposed reductions, achieving smaller, more deterministic automata with practical runtimes. Overall, the framework demonstrates practical benefits for knowledge-driven verification and points to future work on broader bound-based reductions and knowledge acquisition strategies.

Abstract

We consider the problem of the verification of an LTL specification $\varphi$ on a system $S$ given some prior knowledge $K$, an LTL formula that $S$ is known to satisfy. The automata-theoretic approach to LTL model checking is implemented as an emptiness check of the product $S\otimes A_{\lnot\varphi}$ where $A_{\lnot\varphi}$ is an automaton for the negation of the property. We propose new operations that simplify an automaton $A_{\lnot\varphi}$ \emph{given} some knowledge automaton $A_K$, to produce an automaton $B$ that can be used instead of $A_{\lnot\varphi}$ for more efficient model checking. Our evaluation of these operations on a large benchmark derived from the MCC'22 competition shows that even with simple knowledge, half of the problems can be definitely answered without running an LTL model checker, and the remaining problems can be simplified significantly.

Figures (3)

• Figure 1: The outside box represents all words in $\Sigma^\omega$. Each language is depicted as an ellipse, with the language of the system $\mathscr{L}(S)$ inside the knowledge $\mathscr{L}(K)$ but we do not know whether the system language overlaps the negated property language $\mathscr{L}(\lnot\varphi)$. The language $\mathscr{L}(B)$ represented in magenta can be chosen anywhere between these extremes to replace $\mathscr{L}(\lnot\varphi)$ in the model-checking procedure.
• Figure 2: Example of product of $A_{\lnot\varphi}\otimes A_K$ for $\lnot\varphi = \mathsf{F}(a\land c)\lor \mathsf{G}((\mathsf{F} b)\land (\mathsf{F}\bar{b}))$ and $K=\mathsf{F}\mathsf{G}(b)\land \mathsf{G}(c)$. The dashed transitions are those removed by $\mathit{Trim}$. We have $\mathop{\mathrm{\mathsf{SG}}}\nolimits(q_0)=\mathop{\mathrm{\mathsf{SG}}}\nolimits(q_1)=(c)\lor(b\land c)\lor (b\land c)=c$ because these two states can be synchronized with all the states of $A_K$, therefore their state guarantee is the disjunction of all labels of $A_K$. This result indicates that when the system is synchronized with state $q_0$, it will always satisfy $c$. We have $\mathop{\mathrm{\mathsf{TG}}}\nolimits(q_1\xrightarrow{\top,\stacc0\stacc1}q_1) = (c)\lor(b\land c) = c$, which indicates that when a transition of the system is synchronized with this self-loop, it will always satisfy $c$. Finally, $\mathop{\mathrm{\mathsf{TG}}}\nolimits(q_0\xrightarrow{\bar{a}\lor\bar{c},\emptyset}q_2)=\bot$ because the only transition synchronizing with this one was trimmed, showing that this transition is not needed.
• Figure 4: Use of Spot in a Jupyter notebook to integrate some trivial knowledge $K=\bar{a}$ (top right automaton) into the stutter-sensitive automaton for $\lnot\varphi = \mathsf{X}\mathsf{F}(a)$ (top-left automaton) and turn it into a stutter-insensitive automata. Simplified automata for $\mathit{sirestrict}_{|K}(A)$ and $\mathit{sirelax}_{|K}(A)$ are given on the bottom left and right respectively.

Theorems & Definitions (11)

• theorem thmcountertheorem
• definition thmcounterdefinition: TGBA
• theorem thmcountertheorem: TGBA for a formula couvreur.99.fmgastin.01.cavgiannakopoulou.02.forte
• definition thmcounterdefinition: Product of TGBA
• definition thmcounterdefinition: Knowledge-based state guarantee
• definition thmcounterdefinition: Knowledge-based transition guarantee
• theorem thmcountertheorem
• theorem thmcountertheorem: Stutter-Insensitive relaxation and restriction
• proof
• theorem thmcountertheorem