Theorem. Safety-liveness decomposition [ltp-000L]

(from Defining Liveness)

Every property is the intersection of a safety and a liveness property.

Proof.

Let $P$ be a property. Then, let $L$ = $(\overline {P} \setminus P)^\complement$ . Then:

\begin {array}{lcl} L \cap \overline {P} & = & (\overline {P} \setminus P)^\complement \cap \overline {P} \\ & = & (\overline {P}^\complement \cup P) \cap \overline {P} \\ & = & (\overline {P}^\complement \cap \overline {P}) \cup (P \cap \overline {P}) \\ & = & \emptyset \cup (P \cap \overline {P}) \\ & = & P \end {array}

The set $\overline {P}$ is clearly closed and therefore a safety property. It remains to show that $L$ is dense (and therefore a liveness property).

Assume for contradiction that $A = (\overline {P}\setminus P)^\complement$ is not dense, so there exists $\sigma \in \Sigma ^\omega$ such that $\sigma \notin \overline {A}$ . By our definition of safety closure, some finite prefix $u$ of $\sigma$ is a bad prefix of $A$ , meaning no extension of $u$ lies in $A$ . Hence every extension of $u$ lies in $\overline {P} \setminus P$ , i.e. every extension of $u$ lies in $\overline {P}$ but not in $P$ . Because every extension of $u$ lies in $\overline {P}$ , $u$ cannot finitely refute $P$ , so every extension of $u$ must be extendable to some trace in $P$ , contradicting that no extension of $u$ lies in $P$ . Therefore no such $u$ exists, so every behaviour $\sigma$ is in $\overline {A}$ , and $A$ is dense.