# 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 "Looping" 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$$ 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$$.

• thanks for the detailed answer. Do you have some reference in which is discussed this particular case? Feb 23 '21 at 17:42
• I added a reference in the answer. I'm not sure it has a proof of the claim, since the proof is pretty much identical to the case of NFA->DFA translation. Feb 23 '21 at 18:13