<p>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:
<a href="https://faculty.idc.ac.il/udiboker/files/MullerAutomata.pdf" rel="nofollow noreferrer">https://faculty.idc.ac.il/udiboker/files/MullerAutomata.pdf</a></p>
<p>A looping automaton can be described as <span class="math-container">$\left&lt;Q,\Sigma,\delta,Q_0\right&gt;$</span> where the components are states, alphabet, transition function <span class="math-container">$\delta:Q\times \Sigma\to 2^Q$</span> and <span class="math-container">$Q_0$</span> are the initial states. Then, the acceptance condition is that there exists a run on the word. That is, <span class="math-container">$w$</span> is accepted iff the automaton has some run on it.</p>
<p>It is easy to see (using
Kőnig's Lemma) that the acceptance condition can be equivalently described as follows: for a word <span class="math-container">$w\in \Sigma^\omega$</span>, let <span class="math-container">$w_i$</span> be its prefix up to letter <span class="math-container">$i$</span>, then <span class="math-container">$w$</span> is accepted iff <span class="math-container">$\delta^*(Q_0,w_i)\neq \emptyset$</span> for all <span class="math-container">$i\in \mathbb{N}$</span>.</p>
<p>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 <span class="math-container">$\emptyset$</span>.</p>

CC BY-SA 4.0
2021-02-23T17:42:40.887Z
thanks for the detailed answer. Do you have some reference in which is discussed this particular case?
kafka
CC BY-SA 4.0
2021-02-23T18:13:26.497Z
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.
Shaull
CC BY-SA 4.0
2021-01-30T17:57:21.497Z
2021-02-23T18:12:52.883Z
2021-02-23T18:12:52.883Z
Shaull
<p>In <a href="https://ecommons.cornell.edu/bitstream/handle/1813/6567/86-727.pdf?sequence=1" rel="nofollow noreferrer">Alpern,Schneider 86</a> is described how to extract the automata that recognize safety and liveness properties from a Buchi automaton <span class="math-container">$m$</span>. 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 <span class="math-container">$m$</span> accepting. The question is: although it is a Buchi, can this automaton be determinized by using the subset construction?</p>

<automata-theory><linear-temporal-logic><omega-language>
Decomposition of safety and liveness properties
kafka
# Decomposition of safety and liveness properties

(Asked by: username_0 on 2021-01-27)

In [Alpern,Schneider 86](https://ecommons.cornell.edu/bitstream/handle/1813/6567/86-727.pdf?sequence=1) 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?

**Tags:** automata-theory, linear-temporal-logic, omega-language

---

## 1 answers

### Answer by username_1 on 2021-01-30. Score: 3 | Accepted answer

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$.

> **Comments:**
> **username_0**: thanks for the detailed answer. Do you have some reference in which is discussed this particular case?  
> **username_1**: 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.  

---

