$$(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 ?
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}