# LTL Model Checking Exam 14.02.2018

In Problem 7a) for translating LTL formula to an equivalent automaton formula, F[a B b] | [a U (Fc)], why does the solution not have 2 more acceptance conditions ?

GF[q0 | b] & GF[a --> q3]

https://es.cs.uni-kl.de/teaching/vrs/exams/2018.02.14.vrs/2018.02.14.vrs.solutions.pdf

Could someone please explain me the reason.

+1 vote

To translate F[a WB b] ∨ [a WU (F c)] to an equivalent omega-automaton, we will abbreviate

• q0 := [a WB b]
• q1 := F q0
• q2 := F c
• q3 :=  [a WU q2]

Next, we replace these definitions by transition relations and fairness constraints. For each state variable, we would get one fairness constraint:

• q0 yields GF[q0∨b]
• q1 yields GF[q1->q0])
• q2 yields GF[q2->c])
• q3 yields GF[a->q3]

In the example solution, you find the fairness constraints for q1 and q2, but you miss the other two. You may safely add one or both of them if you want, the solution will be correct with them also. However, since they stem from weak operators with positive occurrences, you may omit them also if you want. See the slides of the related chapter that mentions this optimization after the unoptimized procedure has been explained.

by (93k points)
edited by
Thank you for the explanation