Direct conversion from regular expression to MSO

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.

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

• 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

• 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).

StackExchange Computer Science Q#47880, answer score: 7