Doubt in Temporal Logic

Question

For this problem, would this solution be ok? If not, can someone explain how?

 

Answer 1

The two structures do not distinguish between the formula. In the second one all sub-formulas are false on the path, and on the first structure [a SW X[a SB [a WU b]]] holds, while the subformulas [a SB [a WU b]] and [a WU b] are always false.

Comments

I didn't understand exactly. Is the drawn solution wrong?

---

Sorry, my answer was confusing. The drawn solution is not correct since the formula is false on both structures, so that the two structures do not distinguish between the formula.

If a is always true, then [a WU b] is always true as well, and then [a SB [a WU b]] becomes [a SB true] which is always false, so that [a SW X[a SB [a WU b]]] becomes [a SW X false] which is also false. So, the first structure is not satisfying the formula.

---

Thank you so much. Understood it now

---

I think, the simplification for the given formula which I did is wrong. What would be the correct simplification for the given question? It would be really helpful for me to track my mistake.

---

Yes, your simplifications were wrong. There are no real simplifications in this case. What you can do is to apply the recursion laws to unroll the formula so that you can see what needs to hold now and what must not hold now. This gives you a structure that does not satisfy the formula. For satisfying it, you need to follow its semantics.