Open Lecture — Logic and Automata and Beyond

An important theme in logic in computer science is the interplay between logic and automata.  In this theme, the logic of interest is often monadic second-orer logic (mso), which is like first-order logic except that one can also quantify over sets of elements (but not sets of pairs, or sets of triples, etc.).  The classical result is Büchi’s theorem: it is decidable if a sentence of mso is true in the structure (N,<) of natural numbers with an order (but with no arithmetic structure, like addition).  Büchi’s theorem has been very influential, especially its proof, which says that every formula of mso can be effectively translated to an equivalent finite-state automaton (over infinite words).  This idea, now called “the automata method”, has been applied in many settings, leading to notions of automata for trees, graphs, infinite trees, etc. 

Apart from these classical results, in my talk I will also describe some recent work, which aims to see if the automata method can work for any logic beyond mso.  It is very difficult to add anything to mso and still retain decidability.  I will survey some feeble attempts in this direction, including logics that talk about probability or boundedness, together with their associated automata models.