# Decomposition of safety and liveness properties

In Alpern,Schneider 86 is described how to extract the automata that recognize safety and liveness properties from a Buchi automaton $$m$$. This shows that any property rapresented by a Buchi automaton is equivalent to the intersection of these two automata. In particular, the automata for the safety properties is represented by making all states of $$m$$ accepting. The question is: although it is a Buchi, can this automaton be determinized by using the subset construction?

A looping automaton can be described as $$\left$$ where the components are states, alphabet, transition function $$\delta:Q\times \Sigma\to 2^Q$$ and $$Q_0$$ are the initial states. Then, the acceptance condition is that there exists a run on the word. That is, $$w$$ is accepted iff the automaton has some run on it.
It is easy to see (using Kőnig's Lemma) that the acceptance condition can be equivalently described as follows: for a word $$w\in \Sigma^\omega$$, let $$w_i$$ be its prefix up to letter $$i$$, then $$w$$ is accepted iff $$\delta^*(Q_0,w_i)\neq \emptyset$$ for all $$i\in \mathbb{N}$$.
This shows that it's enough to track the subset construction in order to determine acceptance. What you end up is a deterministic automaton whose states are all accepting except for one, that corresponds to $$\emptyset$$.