Expressing finite automaton in WS1S
Consider a finite automaton with alphabet , states , transition relation , initial state and final states .
Let the sets denote the encoding of input string of the automaton.
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 :
Then the word is accepted if the above formula holds for the entire input