0
$\begingroup$

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?

$\endgroup$
3
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.