(A sequel to SAV07 Lecture 15.)

• Finite state machine with epsilon transitions
• Closure properties of finite state machines
• Regular expression
• Equivalence of finite state machine and regular expression languages

• Using automata to decide Presburger arithmetic
• MSOL over strings

Automata and languages:

• Introduction to the Theory of Computation
• Introduction to Automata Theory, Languages, and Computation

MSOL:

• The MONA Project

More

• LASH Toolset
• Constraint solving and decision problems of first-order theories of concrete domains, by Ralf Treinen