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 autonaton is in the initial state: