0 votes

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 (120 points)

1 Answer

0 votes

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 (92.2k points)

Related questions

Imprint | Privacy Policy