exam 2019.02. Q7.a

Question

Hello,

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

Answer 1

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.

Comments

Thank you for the clarification