Safety Properties

An LT property \(P_{safe}\) over \(\texttt{AP}\) is called a safety property if for all words \(\sigma \in (2^{\texttt{AP}})^{\omega} \setminus P_{safe}\) there exists a finite prefix \(\hat{\sigma}\) of \(\sigma\) such that:

\[ P_{safe} \cap \Big \{ \sigma^\prime \in (2^{\texttt{AP}})^{\omega} \mid \hat{\sigma} \text{ is a finite prefix of } \sigma^\prime \Big \} = \emptyset \]

Any such finite word \(\hat{\sigma}\) is called a bad prefix for \(P_{safe}\). A minimal bad prefix for \(P_{safe}\) denotes a bad prefix \(\hat{\sigma}\) for \(P_{safe}\) for which no proper prefix of \(\hat{\sigma}\) is a bad prefix of \(P_{safe}\). In other words, minimal bad prefixes are bad prefixes of minimal length.

(Baier and Katoen 2008, 112 chap.3 part.3.3.2)

For a transition system \(\texttt{TS}\) without terminal states and safety property \(P_{safe}\):

\[ \texttt{TS} \models P_{safe} \iff \texttt{Traces}(\texttt{TS}) \cap \texttt{BadPref}(P_{safe}) = \emptyset \]

(Baier and Katoen 2008, 114 chap.3 part.3.3.2)

• Model Checking
• Invariants
• Liveness Properties