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

1.1k questions

1.2k answers


538 users

0 votes

Can you please explain the below question? How do we get 'true' in the G(!b) formula here? 

Thank You!

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

1 Answer

0 votes
Best answer
An existential automaton demands that there must be an infinite run that fulfills the acceptance condition. If the acceptance condition is a safety condition, you can always put that into the transition relation which yields then the simple acceptance condition "true". Formally,

Aexists(Q,I,R,Gphi) = Aexists(Q,I,R&phi,true)

In the above case, the transition relation q&!b&q' was used with the initial state q. That means the automaton has only the state {q} with a self-loop that is only enabled if b is false. Hence, all infinite runs are those where b is always false, and therefore nothing else than the existence of such a run is needed.
by (166k points)
selected by
Thank you! now I understood the G(!b). There is another doubt- please explain, In FGa, why have we written acceptance condition Fp to FGp directly?
If you consider the transition relation of that automaton, i.e., p -> a & p', you can see with the state transitions that in the initial state {}, you may either stay or leave to state {p} for any inputs. However, once you are in state {p} the only further transitions possible are those with a self-loop on {p} where input a has to be true.  Hence, switching once to {p} with Fp or remaining there forever with FGp is the same due to the special transition relation. Both Fp and FGp demand that we cannot remain in the initial state {} forever, and leaving it has then the same consequence.
yes, now I understood. Thank you very much.

Related questions

Imprint | Privacy Policy