0 votes

Hello,

Could someone tell me, in the screenshot,  why we have written only two out of 4 GF part of the calculations?

in * TF "Intelligent Systems" by (350 points)

1 Answer

+1 vote
 
Best answer
q1 abbreviates G(q0) and q0 abbreviates [a SU b] and both occurrences are positive. Hence, we can drop the GF constraint for q1, but must use the one for q0. Same way, q2 abbreviates F c and q3 abbreviates [q2 WB a] with both having positive occurrences, and thus, we just need the GF constraint for q2, but not the one for q3.

See also slide 82 of the temporal logic chapter.
by (91.8k points)
selected by
Thank you for the clarification

Related questions

0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
+1 vote
1 answer
asked Feb 12 in * TF "Emb. Sys. and Rob." by daodubasit (790 points)
0 votes
1 answer
Imprint | Privacy Policy
...