This is an old revision of the document!
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 ...