Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

769 questions

886 answers


424 users

0 votes


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 (117k points)
selected by
Imprint | Privacy Policy