Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.
912 questions
1k answers
1.4k comments
441 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])