# August 2018: 7a - LTL to omega

While translating LTL to omega, shouldn't in final output, QF (acceptance condition) contain one GF/buchi for each state variables?

In 7a, there are 4 state variables in questions: F, B, G, SU

But in the solution only 2 GF is shown.

Can you please clarify why only 2 is there not 4 for each?

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

+1 vote

There are four temporal operators, and therefore we abbreviate these with the four state variables, and you may expect now also four fairness constraints. Indeed, we can add the following ones:

1. GF(q0 | b) which stems from q0 := [a WB b]
2. GF(q1 -> q0) which stems from q1 := F q0
3. GF(c -> q2) which stems from q2 := G c
4. GF(q3 -> a) which stems from q3 := [q2 SU a]

However, due to monotonicity of temporal operators, we do not need the fairness constraints for positive occurrences of weak temporal operators like G, WU, WB and negative occurrences of strong temporal operators like F, SU, SB, and therefore, the constraints for q0 := [a WB b] and q2 := G c are not required. It is not wrong adding anyone of them, but they are just redundant and not required. See slides 81-86 of the related chapter.

by (166k points)
selected by