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
  1. automaton A_a accepting Qa(x)
  2. automaton A_val^{x} accepting correct encodings of a
  3. automaton A_b accepting Qb(x)
  4. 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)
  5. automaton for E(x). Q_b(x), projection on x of A_b (3)
  6. determinized and minimized version of (5)
  7. automaton for E(y) x < y, obtained by projection from the x < y automaton in the script
  8. determinized version of (7)
  9. complement of (8)
  10. correct encoding: (2) again
  11. intersection of (9) and (10)
  12. minimization of (11): automaton for last(x)
  13. 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))
  14. last(x) & not(Qb(x)): intersection of (12) and (1)
  15. minimized version of (14)
  16. not(last(x)) & not(Qa(x)): intersection of (8) and (3), already minimal
  17. (last(x) & not(Qb(x))) | (not(last(x)) & not(Qa(x))): union of (15) and (16)
  18. E(x)(last(x) & not(Qb(x))) | (not(last(x)) & not(Qa(x))): projection of (17)
  19. determinized version of (18)
  20. minimized version of (19)
  21. complement of (20): not E(x)(last(x) & not(Qb(x))) | (not(last(x)) & not(Qa(x)))
  22. minimized version of 21
  23. 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