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