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?
Yes. The automata in question are often called &quot;Looping&quot; automata (so you have a keyword to start from).
A possible starting point is the following paper:
https://faculty.idc.ac.il/udiboker/files/MullerAutomata.pdf
A looping automaton can be described as $\left&lt;Q,\Sigma,\delta,Q_0\right&gt;$ 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$.