LARA This is an old revision of the document! Lecture 16 (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 Using automata to decide MSOL over finite strings Regular expressions for automata with parallel inputs Expressing finite automata in MSOL over strings Expressing regular expressions in MSOL over strings Encoding lists using MSOL over strings Tree automata Field constraint analysis 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