# Expressing regular expressions in MSOL over strings

Idea: for each regular expression of a automaton for parallel inputs associate a formula with free variables such that is valid precisely for whose sets of numbers for which

- and are singletons
- the strings given by the parts of that start at position and end at position satisfy regular expression

that the string (finite set from to

... ap1 ... aq1 ... ... ap2 ... aq2 ... ... ... ... ... ... apn ... aqn ...

The construction is by induction on the structure of regular expressions and resembles the description of parsing the string given by a regular expression:

- base cases are easy
- union is disjunction
- concatenation existentially quantifies over middle position
- iteration in quantifies over a set of positions between and at which a string can be broken into strings that satisfy