0
$\begingroup$

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 ?

Thanks

$\endgroup$
  • $\begingroup$ There are a couple of non-equivalent definitions for liveness properties. What are your precise definitions? $\endgroup$ – Shaull Aug 20 at 6:32
  • $\begingroup$ "the good thing will happen" $\endgroup$ – AleWereWolf Aug 20 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 at 10:39
0
$\begingroup$

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.

$\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.