Theorem. Safety properties are closed under finite union [ltp-0009]

Liam O'Connor

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

Proof.

Liam O'Connor

Let $P$ and $Q$ be safety properties. Take any violating behaviour $\sigma \notin P \cup Q$ . Then, $\sigma \notin P$ and $\sigma \notin Q$ . Since $P$ and $Q$ are safety properties, there exist finite prefixes $t$ and $u$ of $\sigma$ such that no extension of $t$ is in $P$ and no extension of $u$ is in $Q$ . Let $v$ be the longer of $t$ and $u$ ; then $v$ is still a prefix of $\sigma$ . Any extension of $v$ is also an extension of both bad prefixes $t$ and $u$ , so it is in neither in $P$ nor $Q$ , and hence not in $P \cup Q$ . Thus the violation of $P$ can be established just by examining the bad prefix $v$ , so $P \cup Q$ is a safety property.