If i take a safety property $SP$ and a liveness property $LP$, is it true that the result of their intersection is a safety property (and not a liveness property) ? Why ?


  • 1
    $\begingroup$ There are a couple of non-equivalent definitions for liveness properties. What are your precise definitions? $\endgroup$
    – Shaull
    Aug 20, 2019 at 6:32
  • $\begingroup$ "the good thing will happen" $\endgroup$ Aug 20, 2019 at 9:00
  • $\begingroup$ Do you mean to say that $L$ is a liveness property if for every finite word $x$, there exists a suffix $y$ such that $xy\in L$? $\endgroup$
    – Shaull
    Aug 20, 2019 at 10:39

1 Answer 1


No, it is not. If you have a look at the Decomposition theorem for example, then you will find, that there are properties you cannot express as neither a SP or LP, but as an intersection of a SP and LP.

There exist such SP and LP, that their intersection is a safety property. For example the property of all possible traces, the result is again the property of all possible traces. Which incidentally is the only property that is both safety and liveness.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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