Invariants

In fact, the above safety properties are of a particular kind: they are invariants. Invariants are LT properties that are given by a condition Φ for the states and require that Φ holds for all reachable states.

(…)

An LT Property P_inv over AP is an invariant if there is a Propositional Logic formula Φ over AP such that:

\[ P_{inv} = \Big \{ A_0 A_1 A_2 \ldots \in (2^{AP})^{\omega} \mid \forall j \geq 0. A_j \models \phi \Big \} \]

φ is called an invariant condition (or state condition) of P_inv.

Note that

\begin{equation} \begin{split} \texttt{TS} \models P_{inv} &\leftrightarrow \texttt{trace}(\pi) \in P_{inv}, \text{ for all paths } \pi \in \texttt{TS} \\ &\leftrightarrow \texttt{L}(s) \models \Phi \text{ for all states s that belong to a path of \texttt{TS}} \\ &\leftrightarrow \texttt{L}(s) \models \Phi \text{ for all states s } \in \texttt{Reach}(\texttt{TS}) \end{split} \end{equation}

Thus, the notion "invariant" can be explained as follows: the condition Φ has to be fulfilled by all initial states and satisfaction of Φ is invariant under all transitions in the reachable fragment of the given transition system.

(Baier and Katoen 2008, 108 chap.3)

• Model Checking
• Safety Properties