w-automata meaning of accepting states set?

Question

How do we translate the w-automaton acceptance condition to the set of accepting states?

For example, in the solution to the question 5b of Aug 27, 2019 exam, the accepting state that is marked, is the state {}, but the acceptance condition is FG !p. Shouldn't it be both the states as from state {p} there is an infinite path on which finally G !p holds (state {p} has an outgoing edge to state {}).

A∃( {p} , ¬p ,( p⇒¬p′  | ( p′ ↔ a ) ), FG ¬p )

 

Comments

Identifying accepting states often leads to two kinds of problems in understanding:

a) It's often hard to understand accepting states coming from NFA/DFA. Accepting states in NFA/DFA are slightly different from accepting states in Omega automata. In both cases, we want to accept words. In both cases, we do so if our word yields an accepting path. In NFA/DFA, this path needs to end in an accepting state. In Omega automata, this path needs to touch this state in a certain temporal pattern. Here, this temporal pattern is FG.

b) Accepting states of an FG-automaton are often confused with states satisfying a property like EFG/EFEG. While both states in the example satisfy the temporal property EFG ¬p, only {}, the state satisfying ¬p, is called an accepting state.

Answer 1

The exam is correct. Look, the acceptance condition is FG!p and states that all infinite runs of the -automaton are accepting where from some point of time onwards, only states satisfying !p are traversed. The automaton has only one state variable p, and therefore the two states {} and {p} where !p holds in the former and p holds in the latter. This does not mean that an accepting path is not allowed to reach state {p}. As long as it finally switches back to state {} and stays there forever, it will be accepting. For example, the automaton accepts the word aaa(!a)^∞ with the run {}{p}{}{p}{}^∞.

Comments

Thank you for your reply. You mentioned accepting paths, however, how does that relate to "accepting states". What is the exact correlation between the typical accepting states in automata theory and the acceptance conditions of w-automata formulas.
For instance, why we mark grey only {} but not {p} since, starting from {p} there's a path that still satisfies FG!p. A first thought might be that you consider runs starting from the intial states. But this exam shows that my supposition is wrong (page 21)

https://es.cs.uni-kl.de/teaching/vrs/exams/2019.02.13.vrs/2019.02.13.vrs.solutions.pdf

because also non initial states are marked grey.

Thanks in advance

---

So you are wondering why {} but not {p} is marked in grey and called an accepting state. The reason is that {} is the only state satisfying ¬p. We call the states satisfying this propositional acceptance condition “accepting states”. If we now want to know whether a path is accepted, we need to consider the temporal acceptance condition. Here, this is FG. If we now have a path from the initial state that touches the “accepting states” after finitely many steps in every step, the path is accepted. Thus, we can have paths not only using the grey accepting states that are accepted.

---

Ok now it's clear. Thank you for your quick answer.