Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.
965 questions
1.1k answers
1.5k comments
451 users
Is this also correct.
In this [a SU b] holds in an infinite loop so globally. whereas Ga does not hold.
So S1 is satisfied and S2 is not.
Yes, that is true which you can check with the LTL prover:
(a&!b) & G( ((a&!b)->X(!a&b)) & ((!a&b)->X(a&!b)) ) -> !((G a) & (F b)) & (G[a SU b])