I know there exists an equation-based method for transforming finite automata into regular language (or `regular expression'). The main idea is as follows. First we construct a set of equations named "(1)" based on an automaton $A$: \begin{equation}\begin{aligned}&l_1 = \varepsilon + p_{11}l_1 + p_{12}l_2 + ... + p_{1n}l_n\\ &l_2 = \varepsilon + p_{21}l_1 + p_{22}l_2 + ... + p_{2n}l_n\\ &...\\ &l_n = \varepsilon + p_{n1}l_1 + p_{n2}l_2 + ... + p_{nn}l_n, \end{aligned}\end{equation} where are $l_1,...,l_n$ are the locations (or called "states") of $A$ with $l_1$ the initial location, $p_{ij}$ are regular expressions. Then we apply Arden's rule:

"$X = p^*q$ is the unique solution for equation $X = q + pX$"

to solve the equations. The result of $l_1$ is the regular expression we want.

Now my question is, is there a similar method for transforming Büchi automata into omega-regular language?


1 Answer 1


Sure. In fact, the translation from Büchi automata to $\omega$-regular expressions is only a small extension of the one for finite-word languages.

Recall that an $\omega$-regular expression is of the form $s_1\cdot t_1^\omega+\ldots+s_k \cdot t_k^\omega$, where all the $s_i$ and $t_i$ are regular expressions.

The translation of an NBW $A$ to such an expression is based on the following observation: let $A_{p,q}$ be the NFA obtained from $A$ by setting $p$ as the initial state, and $q$ as the single accepting state, then $L(A)=\bigcup_{q\in \alpha} L(A_{q_0,q})\cdot L(A_{q,q})^\omega$ where $\alpha$ is the set of accepting states of $A$.

Indeed, a word is accepted by $A$ iff there is a run on it that leads from $q_0$ to an accepting state $q$, that is then visited infinitely often.

So all you need to do is write the equations that correspond to this union. It'll be slightly uglier than those for an NFA, but not much.

  • 1
    $\begingroup$ Thank you, that is the answer I need. $\endgroup$
    – yrZhang
    Commented Apr 26, 2020 at 15:45

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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