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

769 questions

886 answers

1.3k comments

424 users

0 votes

In this question, the solution was F[¬a SU G(a&b)]. I am a bit confused why we have G(a&b) and not just a&b

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

1 Answer

0 votes
by (117k points)
why can't we also say the same for !a i.e. G !a since t0<= t2
I don't get you point, I am afraid. The formula ∀t2. (t0≤t2 ∧ t2<t1 → ¬a[t2]) does not mean G¬a at time t0, since it just says that a is false from t0 up to t1, but does not state that remains false afterwards. So, it is just an [¬a SU ...] at time t0. So why do you think it should be G¬a? The other part of the formula even states that a holds from t1 onwards.
oh i get it now, i misread initially. thanks
Imprint | Privacy Policy
...