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

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.

• Could you define $Closure(\varphi)$? – Shaull Sep 8 '15 at 12:14
• @Shaull: I added the definition. – Ahmed Nassar Sep 8 '15 at 21:33

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.
• Denis. Thanks for your answer. Indeed, the construction was incorrect. I fixed it now, so please let me know if it implies any relationship between regular and $\omega$-regular safety properties. If not, and you know of a settling answer to that question, please point me to any relevant literature on this. – Ahmed Nassar Sep 8 '15 at 22:13