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

862 questions

981 answers

1.4k comments

431 users

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 ?

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

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 (138k points)
selected by
Thanks a lot for the explanation.
Imprint | Privacy Policy
...