Omega Automata 2016 September Exam paper

Question

Question 5(b) on Omega Automata. 

1. In the first part of the question for the omega languages L1 and L2, the language L1 is expressed by the transition relation (Xq1 ↔ a) ∧ (Xq2 ↔ (q1 → ¬b)) ∧ (Xq3 ↔ (q3 ∧ q2)). I am not quite sure about the Xq3 part. From my understanding, I believe q3 is G(a) which is to be written as q3 ↔ a ∧ Xq3. I am not sure why the expression in the transition relation is that of past(G).
2. Also in part c) and d) of the same question, why are L1 ∩ L2 = L1 and why does 'G(a → X¬b) ∧ F(a → [a U ¬b]) = G(a → X¬b) // Since G(a → X¬b) implies F(a → [a U ¬b]).' hold?  

Answer 1

The formula G(PWX((PWX a) → ¬b)) is translated first to a safety automaton:

    G(PWX((PWX a) → ¬b))
    = 
    AUTO(exists,{q1,q2},q1∧q2,(Xq1 ↔ a)∧(Xq2 ↔ (q1 → ¬b)), Gq2)

That far that good, I guess. Next, we have to convert this safety automaton to a FG-automaton which is done as explained on slide 60 of the omega-automata chapter. That will introduce a new state variable q3. There is no PG used in that formula.

L1 = G(a → X¬b)  and L2 = F(a → [a WU ¬b]). Note first that we can rewrite L2 as (F ¬a) | F[a WU ¬b].

Assume L1 holds, i.e., whenever a holds, then b is false next time. In a first case, we never have a, but then we certainly have F ¬a, and thus also L2. Second, if at some point of time, we have a, then by L1, we must also have X¬b there, thus, ¬b at the next point of time. This also implies L2 since at the next point of time where ¬b holds, we also have [a WU ¬b], and thus also F[a WU ¬b].