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 (91.8k points)
selected by

Related questions

0 votes
1 answer
0 votes
1 answer
asked Aug 18, 2020 in * TF "Vis. and Sci. Comp." by Anshu (870 points)
0 votes
1 answer
0 votes
1 answer
Imprint | Privacy Policy
...