Regular expression - write language in MSO 
$$(ab^*a)^*$$ (a) Define this language in MSO
  (b) Decide if this language is definable in first order logic

(b) It seems to be simple. We know that we can't distinguish in $n$ rounds (wit $n$ quantifiers) two linear order with length $2^{n}+1$ and $2^{n}+2$. These two order can be encoded to two words:   $a^{2^{n}+1}$ and $2^{2^{n}+2}$. Then we use formula for words to distinguish these two words (becase exactly one of them belongs to langugage).   
(a)I know that it may be said:  


*

*first consistent block of $a$ has odd length

*last consistent block of $a$ has odd length   

*for each symbol $b$ there are exists two $a$ on the left and on the right

*if between two consistent block of $b$ there are exists some symbol $a$ then there is even number of $a$ in this block


However, writing this as formula MSO is hard for me. Can you help me ?
 A: You can use the following big hammers:
(1) MSO captures exactly the regular languages (Büchi).
(2) FO captures exactly the star-free languages (McNaughton). See also the more detailed page Langage sans étoile.
(3) A regular language is star-free if and only if its syntactic monoid is aperiodic (Schützenberger). Again, for the syntactic monoid, you can also look at the French version Monoïde syntaxique.
For your language $L = (ab^*a)^*$, the transitions of the minimal automaton are
\begin{array}
 &   &1  &2\\
 a  &2  &1\\
 b  &0  &2
\end{array}
and the initial and unique final state is $1$. Its syntactic monoid has 7 elements: $M = \{1, a, b, ab, ba, aba, bab, 0\}$ and is presented by the relations $a^2 = 1$, $b^2 = b$, $bab = 0$. The fact that $a^2 = 1$ shows immediately that $M$ is not aperiodic, and hence $L$ is not $FO$-expressible.
To get a MSO-formula for $L$, you need to specify the properties of the set $X_q$ of positions of the word in which you are in state $q$ ($q = 1, 2$). The formula should be something like this, where of course, $\min$, $\max$ and $x+1$ should be rewritten with FO-formulas:
\begin{align}
  \exists X_1 \ \exists X_2\ \ &X_1 \cap X_2 = \emptyset  \wedge  \forall x\ (x \in  X_1 \vee x \in X_2)\\
 &(\min \in X_1) \wedge (\max \in X_1) \wedge  {}\\
 &(x \in X_1 \wedge \mathbf{a}x) \to (x+1 \in X_2) \wedge  {}\\
  &(x \in X_2 \wedge \mathbf{a}x) \to (x+1 \in X_1) \wedge  {} \\
&(x \in X_2 \wedge \mathbf{b}x) \to (x+1 \in X_2) 
\end{align}
A: Hint. Guess a subset of the $\mathtt a$s that you pretend are $\mathtt c$s instead, and recognize $(\mathtt a \mathtt b^* \mathtt c)^*$.
