1
$\begingroup$

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.

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

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.

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Ahmed Nassar Sep 8 '15 at 22:13
  • $\begingroup$ With the new definitions the answers are all yes, but it is really not research-level and should rather be on cs.stackexchange. $\endgroup$ – Denis Sep 8 '15 at 22:29

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.