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

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

<p>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.</p>

<p>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.</p>

CC BY-SA 3.0
2015-09-08T22:13:48.530Z
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
CC BY-SA 3.0
2015-09-08T22:29:48.330Z
With the new definitions the answers are all yes, but it is really not research-level and should rather be on cs.stackexchange.
Denis
CC BY-SA 3.0
2015-09-08T14:37:18.240Z
2015-09-08T14:37:18.240Z
Denis
<p>I have two questions:</p>

<p>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 <strong><em>complement</em></strong> of NFA $\overline{\mathcal{A}}^{\varphi} = (Q, \Sigma, \rightarrow, I, F_1 )$:</p>

<p>For every state $q \in Q$, if there <strong><em>is</em></strong> 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.</p>

<p><strong>N.B.</strong> A SCC consisting of a single state with a self-loop is considered nontrivial SCC.</p>

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

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

<blockquote>
  <p>Is $\psi = Closure(\varphi)$?</p>
</blockquote>

<p>According to <a href="https://mitpress.mit.edu/books/principles-model-checking" rel="nofollow">PMC</a>, $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.</p>

<p>Sorry for the elementary question.</p>

CC BY-SA 3.0
2015-09-08T12:14:33.947Z
Could you define $Closure(\varphi)$?
Shaull
CC BY-SA 3.0
2015-09-08T21:33:53.190Z
@Shaull: I added the definition.
Ahmed Nassar
<model-checking><program-verification><temporal-logic><omega-language>
Regular safety properties and bad prefixes of $\omega$-regular properties
Ahmed Nassar
# Regular safety properties and bad prefixes of $\omega$-regular properties

(Asked by: username_0 on 2015-09-07)

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](https://mitpress.mit.edu/books/principles-model-checking), $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.

**Tags:** model-checking, program-verification, temporal-logic, omega-language

> **Comments:**
> **username_1**: Could you define $Closure(\varphi)$?  
> **username_0**: @username_1: I added the definition.  

---

## 1 answers

### Answer by username_2 on 2015-09-08. Score: 2 | Accepted answer

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.

> **Comments:**
> **username_0**: username_2. 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.  
> **username_2**: With the new definitions the answers are all yes, but it is really not research-level and should rather be on cs.stackexchange.  

---

