This is a 3 part tutorial about logic. It is organised around algorithms for checking if a formula is true in a model.There are two central variants of this problem. In the model checking problem

   

we are given the model and the formula, and we want to know it the formula is true in the model. In the satisfiability (dually, validity) problem

   

we are only given the formula, and we want to know if it is true in some (dually, every) model (perhaps from some fixed class of models).

There are three parts of the tutorial (each set of slides contains a soundtrack):

1. Part 1 (slides ) discusses the variant of the model checking problem where the model is fixed and only the formula is given on the input. (This is also known as deciding the theory of the model.)  I will particularly focus on cases where the problem can be solved using automata, and hence the corresponding logic is going to be monadic second-order logic, which is an old friend of automata.
2. Part 2 (slides) discusses the satisfiability problem. Here, again, the main focus is on variants of the problem that can be solved using automata, namely monadic second-order logic on words, trees and graphs of bounded treewidth.
3. Part 2 (slides) discusses the variant of the model checking problem where the formula is fixed and the model is the input. Apart from results that use automata (mainly Courcelle’s theorem about MSO model checking on graphs of bounded treewidth), I will also discuss some results about first-order logic on sparse graph classes.

There is also an abbreviated one-part version, without a soundtrack.