A safety property says that a bad thing does not happen. The "bad thing" in this case is some finite, observable event. In other words, safety properties are those properties whose violation can be established by examining only a finite prefix of the behaviour.

For example, the safety property "The state \mathtt {a} is never reached" is violated by any finite prefix containing the state \mathtt {a}.

The empty property \emptyset and the property \Sigma ^\omega are both safety properties.

The union of any two safety properties is a safety property.

Consider the family of properties P_{i \in \mathbb {N}} = \{ \sigma \in \Sigma ^\omega \mid \sigma _i = \texttt {a}\}, i.e. the property where the ith state is \texttt {a}. Each P_i is a safety property, as all violating behaviours are extensions of bad prefixes of length i. Their union \bigcup _{i \in \mathbb {N}} P_i, however, is not a safety property, as any finite prefix can be extended to a good prefix by appending an \texttt {a}-state, and therefore cannot be a bad prefix.

For a (possibly infinite) collection of properties P_{i \in I}, if every P_i is a safety property then \bigcap _{i \in I} P_i is a safety property.

A guarantee (or cosafety) property is the complement of a safety property. A guarantee property says that a good thing happens eventually. As with safety properties, the "good thing" is some finite, observable event. In other words, guarantee properties are those properties whose satisfaction can be established by examining only a finite prefix of the behaviour.

For example, the guarantee property "The state \mathtt {a} is eventually reached" is satisfied by any finite prefix containing the state \mathtt {a}.

Leslie Lamport originally called these liveness properties, but we use the more popular definition of that term from Alpern and Schneider.

The empty property \emptyset and the property \Sigma ^\omega are both guarantee properties.

The intersection of any two guarantee properties is a guarantee property.

Consider the family of properties P_{i \in \mathbb {N}} = \{ \sigma \in \Sigma ^\omega \mid \sigma _i \neq \texttt {a}\}, i.e. the property where the ith state is not \texttt {a}. Each P_i is a guarantee property, as all satisfying behaviours are extensions of good prefixes ending in a non-\mathtt {a} state of length i. Their intersection \bigcap _{i \in \mathbb {N}} P_i, however, is not a guarantee property, as any finite prefix can be extended to a bad prefix by appending an \texttt {a}-state, and therefore cannot be a good prefix.

For a (possibly infinite) collection of properties P_{i \in I}, if every P_i is a guarantee property then \bigcup _{i \in I} P_i is a guarantee property.

Follows from Counterexample [ltp-000H]. As each P_i is a guarantee property, the guarantee kernel of each P_i is just P_i. But the guarantee kernel of their infinite intersection \bigcap _{i \in \mathbb {N}} P_i is \empty .

The safety closure distributes over binary union, i.e. \overline {P} \cup \overline {R} = \overline {P \cup R}

Follows from Counterexample [ltp-000E]. As each P_i is a safety property, the safety closure of each P_i is just P_i. But the safety closure of their infinite union \bigcup _{i \in \mathbb {N}} P_i is \Sigma ^\omega .

Take the properties P = \{ \sigma \mid \texttt {a}\ \text {occurs infinitely often in}\ \sigma \} and R = \{ \sigma \mid \texttt {a}\ \text {occurs finitely many times in}\ \sigma \}. Both have a safety closure of \Sigma ^\omega , i.e. \overline {P} = \overline {R} = \Sigma ^\omega , however P \cap R = \emptyset so the safety closure of the intersection is \emptyset , not \Sigma ^\omega .

The topological space of properties is a metric space by the following metric, standard for Cantor or Baire spaces:

The function d is a valid metric as d(\sigma ,\rho ) = 0 iff \sigma = \rho , d is symmetric, and the triangle inequality holds: d(\sigma ,\rho ) \leq d(\sigma ,\tau ) + d(\tau ,\rho )

A liveness property says that a good thing happens eventually, but unlike guarantee properties, the "good thing" need not be some finite, observable event. Rather, liveness properties are those properties whose violation cannot be established by examining only a finite prefix of the behaviour. In other words, P is a liveness property iff for any finite prefix t \in \Sigma ^\ast , there exists an infinite extension \sigma \in \Sigma ^\omega such that t\sigma is in the property P.

For example, the property "Every \mathtt {r}equest state is eventually followed by an \mathtt {a}nswer state" is a liveness property: No matter how many unanswered \mathtt {r}equests are in a finite prefix, we could always see the \mathtt {a}nswer in the future.

For a (possibly infinite) collection of properties P_{i \in I}, if every P_i is a liveness property then \bigcup _{i \in I} P_i is a liveness property.

Take the properties P = \{ \sigma \mid \texttt {a}\ \text {occurs infinitely often in}\ \sigma \} and R = \{ \sigma \mid \texttt {a}\ \text {occurs finitely many times in}\ \sigma \}. Both are liveness properties, i.e. dense (\overline {P} = \overline {R} = \Sigma ^\omega ), however P \cap R = \emptyset which is not a liveness property (as \overline {\emptyset } = \emptyset not \Sigma ^\omega ).

Properties are commonly written using linear-time temporal logic (LTL), a modal logic defined over behaviours. Given atomic propositions \mathsf {a} : \Sigma \rightarrow \mathbb {B}, the syntax for formulae is given by:

To assign semantics, we compositionally map each formula to a property. Here the notation f^k indicates the self-composition of f k times, i.e. f^0(x)=x and f^{k+1}(x)=f^k(f(x)). The function \mathop {\triangleright }, the prepend operator, is defined as follows:

These semantics are sometimes written in terms of a satisfaction relation like \sigma \models \varphi . This notation is equivalent to our \sigma \in \llbracket \varphi \rrbracket .

All of the connectives linear-time temporal logic can be constructed from the following minimal fragment (among others:)

The remaining connectives can be derived by using the following identities:

• \bot \equiv \neg \top
• \varphi \lor \psi \equiv \neg (\neg \varphi \land \neg \psi )
• \mathop {\raisebox {-0.2em}{\text {\Large ◇}}} \varphi \equiv \top \mathbin {\mathcal {U}} \varphi
• \mathop {\raisebox {-0.1em}{\text {\Large □}}} \varphi \equiv \neg \mathop {\raisebox {-0.2em}{\text {\Large ◇}}} \neg \varphi
• \varphi \mathbin {\mathcal {R}} \psi \equiv \neg (\neg \varphi \mathbin {\mathcal {U}} \neg \psi )

If P is a decision property then so is P^\complement .

If P and Q are decision properties then so is P \cup Q and P \cap Q.

Follows from Counterexample [ltp-000E]. Each P_i is both a safety property and a guarantee property. Therefore, each P_i is a decision property. But the safety closure of their infinite union \bigcup _{i \in \mathbb {N}} P_i is the strictly larger set \Sigma ^\omega . Therefore, their infinite union is not even a safety property so certainly not a decision property.

Therefore, decision properties are not closed under infinite union. Because decision properties are closed under complement, they cannot be closed under infinite intersection either.