Regular safety properties and bad prefixes of $\omega$-regular properties

Question

I have two questions:

By starting with a nondeterministic Büchi automaton (NBA) $\mathcal{A}^{\varphi} = (Q, \Sigma, \rightarrow, I, F )$ for an $\omega$-regular property $\varphi$, we can construct a NFA $\widehat{\mathcal{A}}^{\varphi} = (Q^{\prime}, \Sigma, \rightarrow^{\prime}, I^{\prime}, F^{\prime} )$ that recognizes the bad prefixes of $\varphi$ as the complement of NFA $\overline{\mathcal{A}}^{\varphi} = (Q, \Sigma, \rightarrow, I, F_1 )$:

For every state $q \in Q$, if there is a nontrivial strongly connected component (SCC) $C \subseteq Q$ such that $C \cap F \neq \emptyset$ and $C$ is reachable from $q$, then $F_1 \leftarrow F_1 \cup \{q\}$. Basically, $q$ is in $F_1$ iff the language of $\mathcal{A}^{\varphi}$ starting from $q$ is nonempty.

N.B. A SCC consisting of a single state with a self-loop is considered nontrivial SCC.

Does NFA $\widehat{\mathcal{A}}^{\varphi}$ recognize all bad prefixes of $\varphi$ and, hence, $\omega$-regular safety properties are regular safety properties, where a safety property is regular if its set of bad prefixes is a regular language?

By determinizing and complementing $\widehat{\mathcal{A}}^{\varphi}$, we can get a NBA $\mathcal{B}^{\psi}$.

Is $\psi = Closure(\varphi)$?

According to PMC, $Closure(\varphi)$ of a linear-time property $\varphi \subseteq \Sigma^{\omega}$ is the set of all infinite words whose finite prefixes are also prefixes of $\varphi$. This coincides with the notion of closure from topology, and $Closure(\varphi)$ will always be a safety property.

Sorry for the elementary question.

Answer 1

Your construction for bad prefixes is not correct on NBA's. For instance take the NBA on alphabet $A=\{a,b\}$ with two initial states $q_a$ and $q_b$ where for both $x\in A$, $q_x$ goes to an accepting sink if the first letter is $x$ and to a rejecting sink if the first letter is not $x$.

Then the language recognized is $A^\omega$, but the set of "bad prefixes" you compute is $A^*$ i.e. all finite words.

Your construction works if you first determinize the automaton. Then the new final states are the ones which cannot reach a component $C$ accepting some infinite word. Careful though, the deterministic automaton is no longer Büchi, it is a parity automaton, so it is a little more complicated to check if a component has empty language.

As for your question about closure, you are essentially asking if for any regular language $L$, $Closure(L)$ is the set of words containing no bad prefixes of $L$. This is true: a word is in the closure of $L$ iff it is arbitrarily close to words in $L$ iff it does not contain a bad prefix.