draw accepting states from w-automaton

Question

In the VRS exam from 16th Feb 2022 the LTL model checking problem, we get the following w-automaton. We know how to translate and draw the transition diagram except for the accepting states. How do we know what the accepting states are?

Answer 1

When we have a NDet-G, NDet-F, NDet-FG or NDet-GF automaton then the accepting states are defined by the acceptance conditions G phi, F phi, FG phi, and GF phi as the set of states that satisfy phi. In the above case, there is a set of sets of accepting states, and we may list the union in the graph, but we should better use different colors for each particular state set. So, we get the accepting states always from the acceptance conditions.

Comments

Thank you, but I'm still confused. As far as I understand the acceptance condition is GF(a->q1)&GF(q0->q2) but how do I get from there to the accepting states in the diagram (which I assume are the green ones)?

---

I don't think that the green states in the figure are the accepting states. That must be some other meaning. It rather seems to me that these are the reachable states without finally deadend states. Therefore, only the green states matter and you may ignore the others.