<p>Safety properties are closed under finite intersection. This can be seen by following Alpern and Schneider's characterisation which showed that safety properties are limit-closed when viewed topologically.</p>

<p>Liveness properties as defined by Alpern and Schneider are dense. They are not closed under intersection as soon as there are two elements in the state space. Consider the two-element state space <span class="math-container">$\{0,1\}$</span>. For state <span class="math-container">$i$</span> define <span class="math-container">$a_i$</span> as the set of infinite sequences of states that have a suffix consisting of <span class="math-container">$i$</span> only. Each <span class="math-container">$a_i$</span> is a liveness property but <span class="math-container">$a_0 \cap a_1 = \emptyset$</span> cannot be a liveness property because it's not dense.</p>

CC BY-SA 4.0
2019-04-14T12:36:27.780Z
2019-04-14T12:36:27.780Z
Kai
<p>Given two safety properties <span class="math-container">$P_1$</span> and <span class="math-container">$P_2$</span>, is their intersection <span class="math-container">$P_1 \cap P_2$</span> also a safety property? Similarly, if <span class="math-container">$P_1$</span> and <span class="math-container">$P_2$</span> are liveness properties, is <span class="math-container">$P_1 \cap P_2$</span> also a liveness property?</p>

<model-checking><temporal-logic>
Are both safety and liveness properties closed under finite intersection?
kauray
# Are both safety and liveness properties closed under finite intersection?

(Asked by: username_0 on 2019-04-13)

Given two safety properties $P\_1$ and $P\_2$, is their intersection $P\_1 \cap P\_2$ also a safety property? Similarly, if $P\_1$ and $P\_2$ are liveness properties, is $P\_1 \cap P\_2$ also a liveness property?

**Tags:** model-checking, temporal-logic


---

## 1 answers

### Answer by username_1 on 2019-04-14. Score: 4 | Accepted answer

Safety properties are closed under finite intersection. This can be seen by following Alpern and Schneider's characterisation which showed that safety properties are limit-closed when viewed topologically.

Liveness properties as defined by Alpern and Schneider are dense. They are not closed under intersection as soon as there are two elements in the state space. Consider the two-element state space $\{0,1\}$. For state $i$ define $a\_i$ as the set of infinite sequences of states that have a suffix consisting of $i$ only. Each $a\_i$ is a liveness property but $a\_0 \cap a\_1 = \emptyset$ cannot be a liveness property because it's not dense.


---

