Analyzing Logics Using Automata

For expressive logics such as first-order logic, key analysis problems, such as whether a sentence is satisfiable, or whether one sentence follows from another, are undecidable. There are two standard responses to regain decidability: one can restrict the structures considered or one can restrict the logic. A surprising development is that these two kinds of restrictions are interconnected. In particular, one can obtain decidable logics (with no restriction on the structures) using decidability results that restrict the structures.

In this course, we follow the development of this idea from work in modal logic that is several decades old, to more recent examples representing some of the most expressive decidable logics. We describe how finite automata are the key to reasoning about logics on restricted structures like trees, and how unravellings and simulations are the key to transferring these results to general structures.