# Translation of LTL to Omega Automata (2021-02-17 6b)

In this solution, The negation of [a SU b ] | [!a WB b] just flips the OR to an AND and the remaining formula remains the same. Which is why the initial states are written as !(q0 | q1). I cant figure out a reason why the acceptance condition is stated the way it is. I cannot find an explanation for how it's reduced to GF(b | q1). Maybe i'm missing a point?

+1 vote

To prove that [a SU b] | [!a WB b] is valid, we prove that its negation !([a SU b] | [!a WB b]) is unsatisfiable. To this end, we translate the latter to an equivalent omega automaton and prove that it cannot accept any word.

To translate !([a SU b] | [!a WB b]) to an omega-automaton, we abbreviate the subformulas [a SU b] and [!a WB b] with state variables q0 and q1, respectively, so that the formula becomes our initial state formula !(q0 | q1). Next, we have to add transition relations and acceptance conditions so that q0 and q1 behave exactly as [a SU b] and [!a WB b], respectively.

Slide 72 of the temporal logic chapter tells us the following

• G[q↔[φ SU ψ]] ⇔ G[q↔ψ∨φ∧Xq]∧GF[q→ψ]
• G[q↔[φ WB ψ]] ⇔ G[q↔¬ψ∧(φ∨Xq)]∧GF[q∨ψ]

Instantiated for our case, this becomes

• G[q0↔[ a SU b]] ⇔ G[q0↔b∨a∧Xq0]∧GF[q0→b]
• G[q1↔[!a WB b]] ⇔ G[q1↔!b∧(!a∨Xq1)]∧GF[q1∨b]

Hence, the omega-automaton has the transition relation (q0↔b∨a∧Xq0) ∧ (q1↔!b∧(!a∨Xq1)) and the acceptance condition GF[q0→b] ∧ GF[q1∨b] so that it looks finally as follows:

```    AUTOexists(
{q0,q1},
!(q0∨q1)
(q0↔b∨a∧Xq0) ∧ (q1↔!b∧(!a∨Xq1)),
GF[q0→b] ∧ GF[q1∨b]
)
```

That above automaton is fine as it is, and could be used as it is. Since q0 represents a strong operator and has a negative occurrence, we may however neglect the acceptance condition GF[q0→b] since it is redundant (see slides 81 and following). Hence, we may simply use

`    AUTOexists(`
```        {q0,q1},
!(q0∨q1)
(q0↔b∨a∧Xq0) ∧ (q1↔!b∧(!a∨Xq1)),
GF[q1∨b]
)```

Having explained all that, I have to mention that the above procedure is explained in full detail on the slides in the chapter about temporal logics, and a couple of examples are presented there also. You should have read and understood that before looking at exercises. Have you read it already?

That part of the exercise is just the application of the standard translation which is straightforward. The remaining part is more interesting since it remains to check that the above automaton does not accept any word. To that end, you have to check that no path starting in an initial state can satisfy GF[q1∨b].

by (166k points)
edited by
It all made sense to me and i had solved it. The only part that was confusing was why the GF[q0→b] was dropped. If we were to use the original solution with the conjunctive condition, it'd be fine too?

Thanks a lot for the answer.
Sure, that is correct as well.