This is an old revision of the document!
Expressing finite automaton in MSOL over strings
Consider a finite automaton with alphabet , states
, transition relation
, initial state
and final states
.
There exists an execution of an automaton iff there exist the intermediate states given by transition relation . We describe intermediate states using sets
, one for each state of the in
. The state
is the set of positions in the execution at which the automaton is in state
. We encode the transition relation
using the formula
Initially, the automaton is in the initial state:
and at some final position it should be in final state:
To express the property that an automaton accepts a string whose length is given by free variable we then use formula
Note: we need to take care of the end of the string as well, by introducing the set of all positions in the input string.