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

+1 vote

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?

in * TF "Emb. Sys. and Rob." by (130 points)

1 Answer

+1 vote

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:

by (170k points)
Imprint | Privacy Policy
...