# LTL model checking exam 16.02.2022

0 votes

Exam question 16.02.2022 Q 6 (a) : 2022.02.16.vrs.solutions.pdf (uni-kl.de)

Why GF(q0 -> !a) suppressed in acceptance condition in the exam solution ?

My solution :

Could you please explain how it is suppressed or removed ?

## 1 Answer

+1 vote

Best answer
This is explained on slides 81-83 of the temporal logic chapter. The point is that we can neglect the fairness constraint for positive occurrences of [φ WU ψ] we can neglect the fairness constraint for negative occurrences of [φ SU ψ] and that carries over to the other operators that are defined as syntactic sugar. As Fψ is  defined as [true SU ψ], we can neglect the fairness constraint for negative occurrences of Fψ. The occurrences of the operators F U and G in the formula are all behind a negation, so they are all negative occurrences. Hence, we can omit the fairness constraint of the F operator (but adding it is also correct).
by (139k points)
selected by
Thanks a lot for the explanation.

0 votes
1 answer
0 votes
1 answer
0 votes
2 answers
0 votes
1 answer
0 votes
1 answer