Unsafe states in NDET G.

Question

Hi,

in the algorithm to determinize NDETG w-automata, it is said to remove unsafe states. How are they formally defined? I suppose if the acceptance condition is of the form Gphi, then it is all the states where !phi holds or if phi is a transition, states where no phi transition exists. Am i right?

Answer 1

Acceptance conditions are properties of states, i.e., the acceptance condition of a safety automaton is a set of states which we call the safe states. Hence, if the acceptance condition is G phi, then the states satisfying phi are the safe ones and those satisfying !phi are the unsafe one.

There are also omega-automata where acceptance conditions refer to transitions instead of states (we actually use these for the translation from LTL to omega automata), but these automata are not more powerful than the traditional ones where acceptance conditions are defined on state sets only.

Comments

Thank you for your answer.I am a bit confused about the acceptance condition refering to transitions instead of states, we used them for example in the automata for GFphi & GFpsi. Does this have an effect at the end for model checking with the mu calculus or does the product structure construction take care of everything implicitly?

---

For model checking that is no problem. Recall that transitions of automata become the states of the Kripke structures.