Automata and Formal Languages: Examples
Note: This is an archvied version of our old webpage. Some links might be broken. The current one can be found here.
Monadic second-order logic over words
This is an example constructing a minimal DFA
from an MSO formula accepting the same language as the formula. It
is a direct application of the construction found in the equivalence
proof (regular lang <-> MSO definable).
A formula for the language L(a*b) is given by
E(x). Qb(x) & A(x) ( (last(x) -> Qb(x)) & (not(last(x)) -> Qa(x)) )
or equivalently by
E(x). Qb(x) & not E(x) ( (last(x) & not(Qb(x))) | (not(last(x)) & not(Qa(x))) )
where last(x) := not E(x).x < y
- automaton A_a accepting Qa(x)
- automaton A_val^{x} accepting correct encodings of a
- automaton A_b accepting Qb(x)
- automaton for not(Qa(x)): obtained by complementing A_a (1) and intersecting with A_val^{x} (2).
If this automaton is minimized one obtains A_b (3)
- automaton for E(x). Q_b(x), projection on x of A_b (3)
- determinized and minimized version of (5)
- automaton for E(y) x < y, obtained by projection from the x < y automaton in the script
- determinized version of (7)
- complement of (8)
- correct encoding: (2) again
- intersection of (9) and (10)
- minimization of (11): automaton for last(x)
- complement of (12): if this automaton is intersected with the correct encoding, one
obtains automaton (8) for E(y) x < y. This is indeed not(last(x))
- last(x) & not(Qb(x)): intersection of (12) and (1)
- minimized version of (14)
- not(last(x)) & not(Qa(x)): intersection of (8) and (3), already minimal
- (last(x) & not(Qb(x))) | (not(last(x)) & not(Qa(x))): union of (15) and (16)
- E(x)(last(x) & not(Qb(x))) | (not(last(x)) & not(Qa(x))): projection of (17)
- determinized version of (18)
- minimized version of (19)
- complement of (20): not E(x)(last(x) & not(Qb(x))) | (not(last(x)) & not(Qa(x)))
- minimized version of 21
- E(x). Qb(x) & not E(x) ( (last(x) & not(Qb(x))) | (not(last(x)) & not(Qa(x))) ) :
intersection of (22) and (6): DFA for L(a*b); in the minimized DFA the initial state
is merged with the other non-final, non-sink state