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<Q,\Sigma,\delta,Q_0\right>$ 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$.

  • $\begingroup$ thanks for the detailed answer. Do you have some reference in which is discussed this particular case? $\endgroup$
    – kafka
    Feb 23 '21 at 17:42
  • 1
    $\begingroup$ 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. $\endgroup$
    – Shaull
    Feb 23 '21 at 18:13

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.