Unsafe state in omega automata

Question

How to identify the unsafe states in omega automata?
e.g:
A∃ ({p}, ¬p, ¬p ∧ a ∨ p ∧ ¬a ∧ ¬p 0 , G(¬p))
A∃ ({p}, ¬p, ¬p ∧ a ∨ p ∧ ¬a ∧ ¬p 0 , G(p)
Is it same for formulas with F(p) / F(¬p) ?
Problem 5 A

Answer 1

I guess that you have a typo in your formulas; and I guess you mean

A∃({p}, ¬p, ¬p ∧ a ∨ p ∧ ¬a ∧ ¬p, G(¬p))
A∃({p}, ¬p, ¬p ∧ a ∨ p ∧ ¬a ∧ ¬p, G(p)

Both of these define the same state transition diagram, i.e., two states that have the following transitions:

Okay, now to your question: Whether a state is safe or unsafe is determined by the acceptance condition of a safety automaton. For your first automaton, the acceptance condition is G(¬p) which declares all states that satisfy ¬p as safe states. That means only state s0 in the above figure, so we must not leave that state. 

In the second automaton, the safe states are those satisfying p which is state s1 only. But since s0 is the initial state, there is no accepting path in that automaton, so it does not accept any word at all.

For liveness automata with acceptance condition F phi, there are no safe state, but states that are must be reached, and Büchi automata have fair states, i.e., a set of states that must be visited infinitely often.

Comments

Thanks for your explanation.

As I am not able to link attachment here, I added a link to a previous paper in the original question.
In problem 5A, why we removed unsafe state, will it be a wrong solution if we draw the automata as mentioned by you?

---

The task there was to determinize the automaton. For safety automata, this is done by first removing all unsafe states, and then by applying the subset construction afterwards. Note also that the transition relation in that problem is different to the one you wrote above, or at least I interpreted it in another way: I used  ¬p ∧ a ∨ p ∧ ¬a ∧ ¬p while the problem mentions ¬p ∧ a ∨ p ∧ ¬a ∧ ¬next(p).

---

Thank you for the explanation. yes I had copied the formula, ' changed to 0 while pasting it. thanks again.