Another Look at LTL Modulo Theory over Finite and Infinite Traces

Linear Temporal Logic is a de facto standard for specification of properties of complex systems. Fundamental problems in formal verification include satisfiability checking and model checking. Extensions and variants of LTL have gained significant interest: with \(\textit{LTL}_f\), the temporal formulas are interpreted over finite traces; with safety fragments of LTL, model checking can be reduced to search for finite trace counterexamples; in the context of Verification Modulo Theories, LTL includes first-order atoms interpreted over background theories. In this paper we propose a symbolic, automata-theoretic approach for these variants of LTL in a general and comprehensive framework, show the correctness of the reduction to liveness and invariant checking, and present a library of open benchmarks and support tools.

1. 1.

   The approach also supports LTL validity and satisfiability checking. \(\models \varphi \) is reduced to a model checking problem \(S_U\models \varphi \), where \(S_U\) is the universal transition system. Satisfiability is obtained by dualization, i.e. \(\varphi \) is satisfiable iff \(S_U\not \models \lnot \varphi \).

2. 2.

   It should be noted that it is possible to restrict the amount of fairness constraint considering only \(\beta _1U\beta _2\in Sub(\phi )\) occurring positively in \(\phi \).

Authors and Affiliations

1. Fondazione Bruno Kessler, Via Sommarive, 18, 38123, Povo, TN, Italy

   Alberto Bombardelli, Alessandro Cimatti, Alberto Griggio & Stefano Tonetta

Corresponding author

Correspondence to Alessandro Cimatti .

Editors and Affiliations

1. Ruhr University Bochum and Radboud University Nijmegen, Bochum, Germany

   Nils Jansen

2. Radboud University Nijmegen, Nijmegen, The Netherlands

   Sebastian Junges

3. Saarland University and University College London, Saarbrücken, Germany

   Benjamin Lucien Kaminski

4. University of Oldenburg, Oldenburg, Germany

   Christoph Matheja

5. RWTH Aachen University, Aachen, Germany

   Thomas Noll

6. RWTH Aachen University, Aachen, Germany

   Tim Quatmann

7. University of Twente and Radboud University Nijmegen, Enschede, The Netherlands

   Mariëlle Stoelinga

8. Eindhoven University of Technology, Eindhoven, The Netherlands

   Matthias Volk

A Proofs

1.1 A.1 Proofs of Section 3

Proof of Theorem 2From validity to model checking:

Proof

To prove the equivalence between the model checking of universal model \(S_U\) and the validity, we show that the set of infinite (resp. finite) traces of \(S_U\) is equal to \(\varPi ^M(V)\) (resp. \(\varPi ^M_f(V)\)).

Let \(S = \{ \pi | \pi \text {is a trace infinite trace of } S_U\}\) and \(S_f = \{ \pi | \pi \text {is a trace finite} {trace of } S_U\}\). \(S = \varPi ^M(V)\) and \(S_f = \varPi ^M_f(V)\)

We split the proof in two parts using set inclusion: one direction is trivial \(Q \subseteq \varPi ^M(V)\) and \(Q^f \subseteq \varPi ^M_f(V)\) since the traces of \(S_U\) are all traces over \(V\).

We prove the other direction by w.o.c. considering an infinite (resp. finite) trace \(\pi \) (\(\pi '\)) s.t. \(\pi \in \varPi ^M(V)\) (\(\pi ' \in \varPi ^M_f(V)\)) and \(\pi \notin Q\) (\(\pi ' \notin Q_f\)). Since \(\pi \) (\(\pi '\)) is not a trace of \(S_U\) then either \(\pi (\pi '), 0 \not \models I_U\) or for all \(0 \le i < |\pi | (|\pi '|) - 1\) \(\pi (\pi ')\not \models T_U\). Since \(I_U = T_U = \top \) from the semantics we obtain that no trace violates \(\top \) by definition contradicting the claim. Therefore, as expected the universal model contains all the traces over \(V\) proving the mapping from validity to model checking.

From model checking to validity:

Proof

(\(\Rightarrow \)):

\(\bullet \):

We want to prove that: \(S \models \varphi \Rightarrow I \wedge GT \rightarrow \varphi \) is valid over \(\textit{LTL} (\mathcal {T})\). By contradiction we say that \(S \models \varphi \) and \(I \wedge GT \rightarrow \varphi \) is not valid over \(\textit{LTL} (\mathcal {T})\). Which means that there is an infinite trace \(\pi \) that violates the formula i.e. \(\pi \models I \wedge GT \wedge \lnot \phi \). However, by satisfaction we derive that \(\pi , 0 \models I\) and forall \(i\ge 0: \pi , i \models T\) from which we derive that \(\pi \) is a trace of S; however, by assumption the infinite traces of S satisfy \(\varphi \) (contradiction).

\(\bullet \):

We want to prove that: \(S \models _{fin} \varphi \Rightarrow I \wedge G(X\top \rightarrow T) \rightarrow \varphi \) is valid over \(\textit{LTL}_f (\mathcal {T})\).

By contradiction we say that \(S \models _{fin} \varphi \) and \(I \wedge G(X\top \rightarrow T) \rightarrow \varphi \) is not valid over \(\textit{LTL}_f (\mathcal {T})\). Which means that there is a finite trace \(\pi \) that violates the formula i.e. \(\pi \models I \wedge G(X\top \rightarrow T) \wedge \lnot \varphi \). However, by satisfaction we obtain that \(\pi , 0 \models I\) and for all \(i\le |\pi | -1: \pi , i \models X\top \rightarrow T\). We can simplify the latter one as for all \(i < |\pi |-1\): \(\pi , i \models T\) since \(X\top \) holds when \(i < |\pi | -1\). As for the case with infinite traces we obtain that \(\pi \) is a trace of S ending up with a contradiction. It should be note that without \(X\top \) a finite trace \(\pi \) disproving the property could have existed; indeed, the \(X\top \) guard is crucial for the correctness of the theorem.

(\(\Leftarrow \)):

\(\bullet \):

We want to prove that: \(I \wedge GT \rightarrow \varphi \) is valid over \(\textit{LTL} (\mathcal {T})\) \(\Rightarrow S \models \varphi \). By contradiction we say that \(I \wedge GT \rightarrow \varphi \) is valid over \(\textit{LTL} (\mathcal {T})\) and there is an infinite trace of S violating \(\varphi \). If immediately follows that being a trace of S satisfies I in the initial state and T at each transition; thus contradicting the claim.

\(\bullet \):

We want to prove that: \(I \wedge G(X\top \rightarrow T) \rightarrow \varphi \) is valid over \(\textit{LTL}_f (\mathcal {T})\) \(\Rightarrow S \models _{fin} \varphi \).

By contradiction we say that \(I \wedge G(X\top \rightarrow T) \rightarrow \varphi \) is valid over \(\textit{LTL} (\mathcal {T})\) and there is a finite trace of S violating \(\varphi \). If immediately follows that being a trace of S satisfies I in the initial state and T at each transition which formally means: \(\pi , 0 \models _{fin} I\) and for all \(0 \le i < |\pi | -1\) \(\pi , i \models T\). Since \(X\top \) is valid iff \(i < |\pi | -1\) then for all \(0 \le i \le |\pi | -1: \pi , i \models X\top \rightarrow T\). From which we show the contradiction.

1.2 A.2 Symbolic Compilation Correctness

Proof of Theorem 7

Definition 9

Let us define the function State taking an LTL formula and a trace \(\sigma \) and returning a set of variables:

• \(State^{sng}(a,\sigma , i)=\emptyset \)

• \(State^{sgn}(\lnot \psi , \sigma , i) = State^{\overline{sgn}}(\psi , \sigma , i)\)

• \(State^{-}(\psi _1\vee \psi _2,\sigma , i)= State^{-}(\psi _1,\sigma , i) \cup State^{-}(\psi _2,\sigma , i)\)

• \(State^{+}(\psi _1\vee \psi _2,\sigma , i)={\left\{ \begin{array}{ll}State^{+}(\psi _1,\sigma , i)& \text { if }\sigma , i\models \psi _1\\ State^{+}(\psi _2,\sigma , i) & \text { else }\end{array}\right. }\)

• \(State^+(\psi _1 U \psi _2,\sigma , i) = {\left\{ \begin{array}{ll}State^+(\psi _2,\sigma , i)& \text { if }\sigma , i \models \psi _2\\ State^+(\psi _1,\sigma , i)\cup \{v_{X(\psi _1 U \psi _2)}\} & \text { else }\end{array}\right. }\)

• \(State^+(Y\psi ,\sigma , i)=\{v_{Y\psi }\}\)

• \(State^+(\psi _1 S \psi _2,\sigma , i) = {\left\{ \begin{array}{ll}State^+(\psi _2,\sigma , i)& \text { if }\sigma , i \models \psi _2\\ State^+(\psi _1,\sigma , i)\cup \{v_{Y(\psi _1 S \psi _2)}\} & \text { else }\end{array}\right. }\)

• \(State^-(\mathcal{O}\mathcal{P}1(\psi ), \sigma , i) = \emptyset \)

• \(State^-((\psi _1) \mathcal{O}\mathcal{P}2 (\psi _2), \sigma , i) = \emptyset \)

where \(sgn \in \{ -, +\}\), \(\overline{sgn} = -\) if \(sgn=+\), \(\overline{sgn} = +\) if \(sng =-\), \(\mathcal{O}\mathcal{P}1 \in \{ X, Y\}\) and \(\mathcal{O}\mathcal{P}2 \in \{ U, S\}\)

Proof

(\(\Leftarrow \)):

\(\exists \pi \) of \(S_{\lnot \varphi }\times S^{deg}_{F_{\lnot \varphi }}\) visiting \(f^l_{\lnot \varphi }\) infinitely often \(\Rightarrow \) \(\sigma \models \lnot \varphi \).

Given a subformula \(\psi \) of \(\lnot \varphi \), we prove that for all \(i\ge 0\), (i) if \(\psi \) occurs positively in \(\lnot \phi \) \(\pi , i\models Enc(\psi )\) implies \(\pi , i \models \psi \); (ii)if \(\psi \) occurs negatively in \(\lnot \phi \): \(\pi , i\models \lnot Enc(\psi )\) implies \(\pi , i \models \lnot \psi \) From this the theorem follows immediately, since the initial state \(\pi , 0\models Enc(\lnot \phi )\). We prove the claim by induction on \(\psi \):

\(\bullet \):

\(\psi = p\): \(\pi , i \models \psi \) by construction

\(\bullet \):

\(\psi = \psi _1 \vee \psi _2\): trivially by induction

\(\bullet \):

\(\psi = \psi _1 \wedge \psi _2\): Trivial induction

\(\bullet \):

\(\psi = \lnot \psi '\). Trivially holds by induction. (if \(\psi '\) occurs negative the subformula occurs positively and vice versa).

\(\bullet \):

\(\psi = X\psi '\): From the transition relation \(\pi , i \models v_{X\psi '}\) iff \(\pi , i+1\models Enc(\psi ')\); thus, \(\pi , i+1 \models \psi '\) by induction.

\(\bullet \):

\(\psi = \psi _1 \, U\psi _2\): We split the two cases (positive, negative occurrence). In the first case, either \(Enc(\psi _2)\) holds or \(Enc(\psi _1)\) holds and \(v_{X(\psi _1 U\psi _2)}\) holds. The first case is managed by induction over \(\psi _2\). For the second case we apply the induction for \(\psi _1\) and, since \(Enc(\psi ) \rightarrow Enc(\psi _2) \in F_{\lnot \psi }\) then there is a point \(k \ge i\) s.t. \(\pi , k \models Enc(\psi _2)\) and (from prophecy variable transition relation) for all \(i \le j < k: \pi , j \models Enc(\psi _1)\); from which we can apply induction and derive the result (for the positive occurrence).

In the other case, \(\pi , i \not \models Enc(\psi _2)\) and either \(\pi , i \not \models Enc(\psi _1)\) or \(\pi , i \not \models v_{X(\psi _1 U\psi _2)}\). By the transition relation we know that \(v_{X(\psi _1 U\psi _2)} \leftrightarrow Enc(\psi _2)' \vee Enc(\psi _1)' \wedge v_{X_{\psi _1 U\psi _2)}}'\); therefore, since \(v_{X(\psi _1 U\psi _2)}\) is violated either there is a point k in the future s.t. \(\psi _1\) is violated and all the points j between i and j violates \(Enc(\psi _2)\) as well or it is never true that \(Enc(\psi _2)\) holds.

We can prove this claim by w.o.c. suppose that exists a \(k\ge i\) s.t. \(\pi , k \models Enc(\psi _2)\) and for all \(i \le j < k: \pi , j \models Enc(\psi _1)\). From the transition relation definition we get that \(\pi , k -1 \models v_{X(\psi _1 U\psi _2)}\). Since by hypothesis in all the index \(i \le j < k: \pi , j \models Enc(\psi _1)\) with a straightforward inductive reasoning down to i we derive that \(\pi , i \models Enc(\psi _1 U\psi _2)\) which contradicts the statement.

Finally, we apply induction to \(Enc(\psi _1)\) and \(Enc(\psi _2)\) and we derive the semantics of the negation of until.

\(\bullet \):

\(\psi = Y\psi '\): \(\pi , i \models v_{Y\psi }\) iff \(i > 0\) (from initial condition) and \(\pi , i-1\models \psi '\) (from transition relation); thus, \(\pi , i \models v_{Y\psi '} \Leftrightarrow i > 0 \text { and }\pi , i-1 \models Enc(\psi ')\). Finally from induction we obtain \(i > 0\) and \(\pi , i-1 \models \psi '\) proving the case.

\(\bullet \):

\(\psi = \psi _1 \, S\psi _2\): we prove this case by induction on i; for the base case, we consider the index 0; in this case, all variables \(v_{Y\beta }\) are false in \(\pi ,0\) and the claim follows trivially; suppose the claim holds for \(i-1\), we prove it for i: \(\pi , i \models v_{Y(\psi _1 \, S\psi _2)}\) iff \(i > 0\) (initial condition) and either \(\pi , i-1 \models \psi _2\) and thus \(\pi , i-1\models \psi _2\) by induction, or that \(\pi , i-1 \models \psi _1 \wedge v_{Y(\psi _1 \, S\psi _2)}\) and thus \(\pi , i-1 \models \psi \) by induction.

\(\Rightarrow \):

\(\sigma \models \lnot \varphi \Rightarrow \exists \pi \) of \(S_{\lnot \varphi }\times S^{deg}_{F_{\lnot \varphi }}\) visiting \(f^l_{\lnot \varphi }\) infinitely often.

Given a trace \(\sigma \) and an LTL property \(\varphi \) such that \(\sigma \models \lnot \varphi \). Let us define the sequence of states \(s_i\) as follows: \(s_0=State^+(Enc(\lnot \varphi ))\); for all \(i>0\), \(s_i=State^+(\bigwedge _{v_{X\beta }\in s_{i-1}}\beta )\). The sequence \(\pi =s_0,s_1,\ldots \) is a path of \(S^l_{\lnot \varphi }\) over the trace \(\pi \). It is easy to see that in each point i if each subformula \(\psi \) is satisfied by \(\sigma \) then \(\pi , i \models State^+(\psi )\). Therefore, for untils \(v_{X(\psi _1 U\psi _2)}\) is true iff in the future there is a point satisfying \(\psi _2\) which guarantees that the degeneralized fairness holds infinitely often.

Proof of Theorem 8

Definition 10

Let us define the function \(State_f\) taking an LTL formula and a trace \(\sigma \) and returning a set of variables:

• \(State_f(a,\sigma , i)=\emptyset \)

• \(State_f(\psi _1\wedge \psi _2,\sigma , i)= State_f(\psi _1,\sigma , i) \cup State_f(\psi _2,\sigma , i)\)

• \(State_f(\psi _1\vee \psi _2,\sigma , i)={\left\{ \begin{array}{ll}State_f(\psi _1,\sigma , i)& \text { if }\sigma , i\models \psi _1\\ State_f(\psi _2,\sigma , i) & \text { else }\end{array}\right. }\)

• \(State_f(X\psi ,\sigma , i)=\{v_{X\psi }\}\)

• \(State_f(N\psi ,\sigma , i)=\{v_{N\psi }\}\)

• \(State_f(\psi _1 U\psi _2,\sigma , i) = {\left\{ \begin{array}{ll}State_f(\psi _2,\sigma , i)& \text { if }\sigma , i \models \psi _2\\ State_f(\psi _1,\sigma , i)\cup \{v_{X(\psi _1 U \psi _2}\} & \text { else}\end{array}\right. }\)

• \(State_f(\psi _1 R\psi _2,\sigma , i) = {\left\{ \begin{array}{ll}State_f(\psi _2,\sigma , i) \cup State_f(\psi _1, \sigma , i)& \text { if }\sigma , i \models \psi _2 \wedge \psi _1\\ State_f(\psi _1,\sigma , i)\cup \{v_{X(\psi _1 R\psi _2}\} & \text { else }\end{array}\right. }\)

• \(State_f(Y\psi ,\sigma , i)=\{v_{Y\psi }\}\)

• \(State_f(\psi _1 S\psi _2,\sigma , i) = {\left\{ \begin{array}{ll}State_f(\psi _2,\sigma , i)& \text { if }\sigma , i \models \psi _2\\ State_f(\psi _1,\sigma , i)\cup \{v_{Y(\psi _1 S\psi _2}\} & \text { else }\end{array}\right. }\)

Proof

(\(\Leftarrow \)):

Given a subformula \(\psi \) of \(\phi \), we prove that for all \(i\ge 0\), if \(\pi , i\models Enc(\psi )\), then \(\pi , i \models \psi \). From this the theorem follows immediately, since the initial state \(\pi , 0 \models Enc(\phi )\).

We prove the claim by induction on \(\psi \):

\(\bullet \):

\(\psi = p\): \(\pi , i \models \psi \) by construction

\(\bullet \):

\(\psi = \psi _1 \vee \psi _2\): Trivial induction

\(\bullet \):

\(\psi = \psi _1 \wedge \psi _2\): Trivial induction

\(\bullet \):

\(\psi = N\psi ':\) \(\pi , i \models v_{N\psi '}\) by construction, then the transition requires, if \(i < |\pi | -1\), that \(\pi , i+1\models _{fin} Enc(\psi ')\); thus, \(\pi , i+1 \models _{fin} \psi '\) by induction; if \(i = |\pi | -1\) then \(\pi , i \models _{fin} N\psi '\) vacuously.

\(\bullet \):

\(\psi = X\psi '\): Identical to the previous if \(i < |\pi | -1\). We can show that when \(v_{X\psi '}\) is true i is not the final assignment. That follows from the assumption that \(\pi \) reaches \(f^b_{\lnot \varphi }\) which is composed of the conjunction of the negation of all the proof obligations including \(v_{X\psi '}\)

\(\bullet \):

\(\psi = \psi _1 \, U\psi _2\): we prove this case by induction on i; for the base case, we consider the index \( = |\pi | -1\) as base case; in this case, all the prophecy variables of \(\phi \) are false in \(\pi , i\) and the claim follows trivially; suppose the claim holds for \(i+1\) (which is guaranteed to stay in the path bounds), we prove it for i: \(\pi , i \models _{fin} v_{X(\psi _1 \, U\psi _2)}\) by construction (\(\psi _2\) does not hold), then the transition requires either that \(\pi , i+1 \models _{fin} Enc(\psi _2)\) and thus \(\pi , i+1 \models _{fin} \psi _2\) by induction, or that \(\pi i+1\models _{fin} Enc(\psi _1) \wedge v_{X(\psi _1 \, U\psi _2))}\) and thus \(\pi , i+1 \models _{fin} \psi \) by induction.

\(\bullet \):

\(\psi = \psi _1 R\psi _2\): The proof is similar to the previous case, the only difference is that in this case in the last state you don’t need \(v_{N(\psi _1 R\psi _2)}\) to be false to prove the property while the inductive case is more or less the same.

\(\bullet \):

\(\psi = Y\psi '\): \(\pi , i \models _{fin} v_{Y\psi }\) by construction, then if \(i > 0\) the transition requires that \(\pi , i-1\models _{fin} \psi '\); thus, \(\pi , i-1 \models _{fin} \psi '\)

\(\bullet \):

\(\psi = \psi _1 \, S\psi _2\): we prove this case by induction on i; for the base case, we consider the index 0; in this case, all variables \(v_{Y\beta }\) are false in \(\pi , 0\) and the claim follows trivially; suppose the claim holds for \(i-1\), we prove it for i: \(\pi , i \models _{fin} v_{Y(\psi _1 \, S\psi _2)}\) by construction, then if \(i > 0\) the transition require either that \(\pi , i - 1\models _{fin} \psi _2 \) and thus \(\pi , i-1 \models _{fin}\psi _2\) by induction, or that \(\pi , i-1 \models _{fin} \psi _1 \wedge v_{ Y(\psi _1 \, S\psi _2)}\) and thus \(\pi , i-1 \models _{fin} \psi \) by induction.

\(\bullet \):

the other cases (\(Z, T\)) are similar to the previous ones.

(\(\Rightarrow \)):

Given a trace \(\sigma \) and an \(\textit{LTL}_f\) property \(\varphi \) with \(\phi = \textsc {nnf}_f(\lnot \varphi )\) such that \(\sigma \models \phi \). Let us define the sequence of states \(s_i\) as follows: \(s_0=State_f(Enc(\lnot \varphi ))\); for all \(i>0\), \(s_i=State(\bigwedge _{v_{X\beta }\in s_{i-1}}\beta )\). The sequence \(\pi =s_0,s_1,\ldots \) is a path of \(S^b_{\lnot \varphi }\) over the trace \(\pi \). Let d be the size of \(\sigma \), then \(\pi , d \models _{fin} f^b_{\lnot \varphi }\)

Proof of Theorem 9

Definition 11

Let us define the function State taking an LTL formula and a trace \(\sigma \) and returning a set of variables:

• \(State(a,\sigma , i)=\emptyset \)

• \(State(\psi _1\wedge \psi _2,\sigma , i)= State(\psi _1,\sigma , i) \cup State(\psi _2,\sigma , i)\)

• \(State(\psi _1\vee \psi _2,\sigma , i)={\left\{ \begin{array}{ll}State(\psi _1,\sigma , i)& \text { if }\sigma , i\models \psi _1\\ State(\psi _2,\sigma , i) & \text { else }\end{array}\right. }\)

• \(State(X\psi ,\sigma , i)=\{v_{X\psi }\}\)

• \(State(\psi _1 U \psi _2,\sigma , i) = {\left\{ \begin{array}{ll}State(\psi _2,\sigma , i)& \text { if }\sigma , i \models \psi _2\\ State(\psi _1,\sigma , i)\cup \{v_{X(\psi _1 U \psi _2}\} & \text { else }\end{array}\right. }\)

• \(State(Y\psi ,\sigma , i)=\{v_{Y\psi }\}\)

• \(State(\psi _1 S \psi _2,\sigma , i) = {\left\{ \begin{array}{ll}State(\psi _2,\sigma , i)& \text { if }\sigma , i \models \psi _2\\ State(\psi _1,\sigma , i)\cup \{v_{Y(\psi _1 S \psi _2}\} & \text { else }\end{array}\right. }\)

Proof

(\(\Leftarrow \)):

Given a subformula \(\psi \) of \(\phi \), we prove that for all \(i\ge 0\), if \(\pi , i\models Enc(\psi )\), then \(\pi , i \models \psi \). From this the theorem follows immediately, since the initial state \(\pi , 0 \models Enc(\phi ')\).

We prove the claim by induction on \(\psi \):

\(\bullet \):

\(\psi = p\): \(\pi , i \models \psi \) by construction

\(\bullet \):

\(\psi = \psi _1 \vee \psi _2\): Trivial induction

\(\bullet \):

\(\psi = X\psi '\): \(\pi , i \models v_{X\psi '}\) by construction, then the transition requires that \(\pi , i+1\models Enc(\psi ')\); thus, \(\pi , i+1 \models \psi '\) by induction

\(\bullet \):

\(\psi = \psi _1 \, U\psi _2\): we prove this case by induction on i; for the base case, we consider the index i in which \(\pi , i\) reaches \(f^b_{\lnot \varphi }\); in this case, all the prophecy variables of \(\phi \) are false in \(\pi , i\) and the claim follows trivially; suppose the claim holds for \(i+1\), we prove it for i: \(\pi , i \models v_{X(\psi _1 \, U\psi _2)}\) by construction (\(\psi _2\) does not hold), then the transition requires either that \(\pi (i+1)\models Enc(\psi _2)\) and thus \(\pi , i+1 \models \psi _2\) by induction, or that \(\pi i+1\models E(\psi _1 \wedge X(\psi _1 \, U\psi _2))\) and thus \(\pi , i+1 \models \psi \) by induction.

\(\bullet \):

\(\psi = Y\psi '\): \(\pi , i \models v_{Y\psi }\) by construction, then if \(i > 0\) the transition requires that \(\pi , i-1\models \psi '\); thus, \(\pi , i-1 \models \psi '\)

\(\bullet \):

\(\psi = \psi _1 \, S\psi _2\): we prove this case by induction on i; for the base case, we consider the index 0; in this case, all variables \(v_{Y\beta }\) are false in \(\pi , 0\) and the claim follows trivially; suppose the claim holds for \(i-1\), we prove it for i: \(\pi , i \models v_{Y(\psi _1 \, S\psi _2)}\) by construction, then if \(i > 0\) the transition require either that \(\pi , i - 1\models \psi _2 \) and thus \(\pi , i-1 \models \psi _2\) by induction, or that \(\pi , i-1 \models \psi _1 \wedge v_{ Y(\psi _1 \, S\psi _2)}\) and thus \(\pi , i-1 \models \psi \) by induction.

\(\bullet \):

the other cases (\(Z, T\)) are similar to the previous ones.

(\(\Rightarrow \)):

Given a trace \(\sigma \) and a safety property \(\varphi \) such that \(\sigma \not \models \varphi \) and \(\phi := \textsc {nnf}(\lnot \phi )\). Let us define the sequence of states \(s_i\) as follows: \(s_0=State(Enc(\phi ))\); for all \(i>0\), \(s_i=State(\bigwedge _{v_{X\beta }\in s_{i-1}}\beta )\). The sequence \(\pi =s_0,s_1,\ldots \) is a path of \(S^b_{\lnot \varphi }\) over the trace \(\pi \). Let d be the size of the bad prefix of \(\sigma \) violating \(\phi \). Then \(\pi , d \models f^b_{\lnot \varphi }\)

Reprints and permissions

© 2025 The Author(s), under exclusive license to Springer Nature Switzerland AG

Policies and ethics