Once you have computed the state transition diagram, the next step is to check whether this automaton can accept any word. Recall that a word is accepted if there is an infinite run that satisfies the acceptance conditions.
We have the following initial states where such a run could start:
s0:{}
s2:{q1}
s4:{q0}
s6:{q0,q1}
However, s2 and s6 are deadend states and therefore have no infinite outgoing path. We can omit them therefore, since from these states no word can be accepted. Also the transition from state {} to state {q2} must not be taken, since {q2} is a deadend state and cannot accept any word. What finally remains are just the two states
- s4:{q0}
- s0:{}
where we have a self-loop for any input in s4:{q0}, a self-loop for input a in s0:{} and a transition from s4:{q0} to s0:{} for input !a. Hence all infinite runs are the following ones:
- s4^omega, i.e., {q0}-*->{q0}-*->...
- s4^*s0^omega {q0}-*->...-*->{q0}-!a->{}-a->{}-a->...
Next, we have to check which of these runs satisfy the acceptance conditions GF(a→q1) ∧ GF(q0→q2). The first path violates GF(q0→q2) since we always have q0, but never q2. The second path violates GF(a→q1) since since have "a" from a certain point of time on, but we never have q1.
The acceptance conditions we obtain for omega automata by the translation from LTL formula are edge automata, i.e., their acceptance conditions refer to edges of the automaton rather than states. GF(a→q1) therefore demands that we have use transitions labeled with !a or starting in q1 infinitely often, and GF(q0→q2) demands that we have to take transitions starting in !q0 or q2 infinitely often.
