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