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
557 users
In state S0, b holds, then there is a path from S0 to S1 where EX EG(!b) holds all the time so should this not satisfy both the formulae? Is there another way to approach to this which I might be missing?
You are right, the solution is not correct. However, note that the EX operator is applied to a disjunction of the formulas EG!b and EGEFa in the first case and EG!b and EGFa in the second case.
A correct solution is as follows: