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

0 votes

Hi,

I don't understand the question and solution very well, what is the difference between Fb and b e.g if b is satisfied so is Fb. Please explain the question and answer so that I can understand. Thanks

 

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

1 Answer

+1 vote
 
Best answer
b just means that b holds at the current point of time, and we don't have any statement about b's value at any other point of time.

F b means that b holds at some time in the future, that may be at time t=0, but also any other point of time.

In the above structure, EG!a holds in states s1 and s0, and since these states do not satisfy b, there is no state satisfying b&EG!a, and therefore also EF(b&EG!a) is nowhere satisfied.

However, S1 is satisfied in state s0, since there is the path s0 s2^omega, that satisfies Fb, and the first state of that path, i.e., s0 satisfies EG!a.
by (170k points)
selected by
Imprint | Privacy Policy
...