# How to interpret acceptance conditions in omega automata

Exam question 16.02.2022 Problem 6 (a) : 2022.02.16.vrs.solutions.pdf (uni-kl.de)

For below description of automata I have drawn the state transition diagram, but little bit confused in how to process these acceptance conditions : Following is the state transition diagram : I interpret GF (a -> q1) as where except the condition that a is true and q1 is false those states will be the accept state. Same goes with another one GF (q0 -> q2) and both needs to be true to be considered as accepting state. Is this right ?

Q. Could you please explain how to do this and is there any concrete way to find the acceptance states based on these types of formula ? (I read the slides but couldn't figured it out properly)

+1 vote

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

1.     s4:{q0}
2.     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:

1.     s4^omega, i.e., {q0}-*->{q0}-*->...
2.     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.

by (162k points)
selected by
Thanks for explaining this in great detail.

So basically when we translate LTL to omega automata there is no need to mark the accepting states because as you said it refers to the edges and not states.
We just need to check for validity of those accepting condition by running it and validating the accepting conditions specified. Is it right ?
Right. But don't worry about the acceptance conditions on edges instead of states, if needed, any edge-based condition can be translated to a state-based one, but that may increase the number of states. Also considering the Kripke structure would not mind about this difference.
Thank you so much for this explanation.