Show description

A sequence of symbols. Such a sequence gives rise to a totally ordered set, a special case of a partially ordered one, which, as we have seen, has a graph-theoretical counterpart. In the following, let Σ be an alphabet. 1 (Word). A word over Σ is a structure w = ({1, . . , n}, , λ), n ∈ IN, where 1, . . , n are the letter positions of w, is the successor relation on {1, . . , n}, which contains the pairs (i, i + 1) with i ∈ {1, . . , n − 1}, and λ is a mapping {1, . . , n} → Σ. The set of words over Σ is denoted by W(Σ) or simply by W if Σ is clear from the context.

This view will be taken and be made more precise in the next section when we (Q) consider automata on (Σ, C)-dags. A transition t = (q, a, q) ∈ Trans (Σ,C) e might be considered to be the Q-extended dag D(t) := (V ∪· {q}, { } ∈C , λ) over (Σ, C) with • V = {(b, ) ∈ Σ × C | q[(b, )] ∈ Q}, = {(b, ) ∈ V | = } × {q} for any ∈ C, • • λ((b, )) = (b, q[(b, )]) for any (b, ) ∈ V , and • λ(q) = (a, q). 2 The Operational Behavior of (Σ, 51 Moreover, q ∈ (Q ∪· {−})Σ×C may be considered to be a subset of (Σ ×Q)×C with the understanding that, for any (a, ) ∈ Σ × C and q ∈ Q, ((a, q), ) ∈ q iff q[(a, )] = q.

FA = MSOW Proof. “⊆”: Suppose A = (S, ∆, sin , F ) to be a finite automaton over Σ, say, with state set S = {s0 , . . , sk } where sin = s0 . Then, for any word w = ({1, . . , n}, , λ) ∈ W(Σ) with w = ε, we have w ∈ L(A) iff w |= ∃X0 . . ∃Xk partition(X0 , . . , to access the first and the last position of a word, respectively. Note that, if the empty word is not recognized by A, one has to add a clause ∃xfirst(x), as, otherwise, ε will be included in the language of the above formula. “⊇”: So let us construct from an arbitrary MSO(Σ, −)-sentence ψ a finite automaton A over Σ such that L(A) = LW(Σ) (ψ).