A language $L \subseteq \Sigma^*$ can be described by a regular expression iff it can be defined by a formula in monadic second order with words as structure $(\{0, \dots, n-1\}, <, (P_a)_{a \in \Sigma})$. The proof I know is an indirection construction over automata, i.e. we show that DFAs and regular expressions / formulas are equivalently powerful.

However, I am interested in a direct transformation process to make analysis of complexity properties easier. If I remember correctly, there is a construction based on the inductive nature of regular expressions and formulas, but I cannot find it. Just a link to a paper presenting these two algorithms (reg.exp. to MSO and back) would suffice for me.

  • $\begingroup$ Union is easy. Concatenation should be based on relativization (formula is true when restricted to certain positions), and star seems transitive closure. But you are asking for explicit references on the corresponding descriptive complexities. Did not find those, sorry. $\endgroup$ Commented Oct 5, 2015 at 13:16
  • $\begingroup$ No, I am not asking for complexities. I am asking for for a detailed description of the constructions. $\endgroup$
    – Andreas T
    Commented Oct 5, 2015 at 13:30

1 Answer 1


The direction from regular expressions to MSO is easy, as MSO is versatile. For a regular expressions $R$ let us construct formulae $\varphi_R$.

$\varphi_{\emptyset} := \bot$

$\varphi_{\varepsilon} := \forall x\bot$

$\varphi_a := \exists x(P_a x \wedge \forall y(x=y))$

$\varphi_{R_1 | R_2} := \varphi_{R_1} \vee \varphi_{R_2}$.

$\varphi_{R_1R_2} := \exists X(\forall y\forall z((Xy \wedge \neg Xz)\to y<z) \wedge [\varphi_{R_1}]_{Xx} \wedge [\varphi_{R_2}]_{\neg Xx})$

$\varphi_{R*} := \exists X(\forall y\forall z(\neg z<y\wedge(\forall x((\neg x<y \wedge \neg z<x)\to(Xx\leftrightarrow Xy))) \wedge \forall x((x<y\wedge(Xx\leftrightarrow Xy))\to\exists x'(x<x'\wedge x'<y\wedge\neg(Xx'\leftrightarrow Xy))) \wedge \forall x((z<x\wedge(Xx\leftrightarrow Xy))\to\exists x'(z<x'\wedge x'<x\wedge\neg(Xx'\leftrightarrow Xy)))) \to [\varphi_R]_{\neg x<y \wedge \neg z<x})$

Here, $[\varphi]_{\psi(x)}$ denotes the relativization of the formula $\varphi$ to the formula $\psi$.

As you can see, the translation is linear.

In the other direction, I suggest to transform MSO to regular expressions in two steps, with NFAs in between. I know this is not what you are asking for. For complexity analysis it should suffice, however: The translation from MSO to NFAs is known not to have any elementary lower bound. And a direct translation to regular expressions cannot be any better, because of the linear translation from regular expressions to NFAs.


Fixed a bug in $\varphi_{R*}$. Also, here follows some explanation of the more complex formulae.

For $\varphi_{R_1R_2}$, the predicate $X$ serves to separate the domain of $R_1$ from the domain of $R_2$. More precisely,

  • $X$ shall hold on a (possibly empty) prefix of the word (The first clause says: all places where $X$ holds come before all places where $\neg X$ holds.).
  • That prefix shall belong to $R_1$ (the second clause does this).
  • The remaining (possibly empty) suffix shall belong to $R_2$ (the third clause says this).

For $\varphi_{R*}$, the predicate $X$ partitions the word into subwords each of which belongs to $R$. These subwords alternatingly belong to $X$ and to $\neg X$. The longish subformula between the $\forall y\forall z$ and the $\to[\varphi_R]_{\neg x<y\wedge\neg z<x}$ says that $y$ and $z$ are the start and end of such a subword:

  • $y\leq z$ (first clause).
  • All positions between $y$ and $z$ agree on whether they belong to $X$ (second clause).
  • If an even lower position also agrees, then there is an intermediate one that doesn't (third clause).
  • If an even higher position also agrees, then there is an intermediate one that doesn't (fourth clause).
  • $\begingroup$ The first clause of the Kleene start translation is confusing me. Is there a resource I can look at that defines this better? $\endgroup$
    – nishantjr
    Commented Oct 9, 2023 at 23:35
  • 1
    $\begingroup$ I don't know of any resource but I have updated the answer $\endgroup$
    – kne
    Commented Oct 11, 2023 at 13:02
  • $\begingroup$ Thank you! Appreciated $\endgroup$
    – nishantjr
    Commented Oct 13, 2023 at 2:48

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.