Theorem. Liveness properties are closed under union [ltp-000T]

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.

Proof.

Let $P_{i \in I}$ be a family of liveness properties. Because liveness properties are dense, for any $i$ , $\overline {P_i} = \Sigma ^\omega$ . As safety closure is monotonic, $\Sigma ^\omega \subseteq \overline {\bigcup _{i \in I} P_i }$ . Therefore the union is dense $\overline {\bigcup _{i \in I} P_i } = \Sigma ^\omega$ and therefore a liveness property.