September 6, 2022, Problem 8.(f)

Question

Does this structure satisfy S2?

For given S2: I tried to consider the next state of the initial state because of X and in the s1 state, I made aSUb true by making the b(the second term in aSUb) globally true.

In the state s0, given S1 doesn't satisfy.

Let me know if my approach is incorrect.

Answer 1

Your solution is correct, since you can prove that the following LTL formula is valid:

!a & !b & X G (!a&b) -> X[a SU b] & ![(X a) SU b]

Comments

Thank you, Professor