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 ?
Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It only takes a minute to sign up.Sign up to join this community
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.