A BRICS Mini-Course
April 9, 11, 16 and 18, 2002
Igor Walukiewicz, email@example.com
Labri, Bordeaux, France
The connections between automata theory and logic are strong and fruitful. Good examples of these are: Buchi's proof of decidability of monadic second-order (MSO) theory of infinite words and Rabin's proof of decidability of MSO theory of infinite binary trees. This last theory is one of the strongest known decidable logical theories with many other decidability results being an easy consequence. Recently, automata play a prominent role in understanding of many logical formalisms used in Computer Aided Verification.
The goal of this mini-course is to show several applications of automata theory in logic. In addition to the results mentioned above we will consider Kamp's theorem for first-order logic and Arnold's recent proof of the mu-calculus hierarchy theorem. While doing this we will have a chance to see some important results in automata theory.
For most of the course we will work with "standard" models like words and trees. At the end we will deal with traces and real-time models.