Overview of course

Logic is one of the cornerstones of computer science. While the beginnings of computer science were intimately related to logic (pioneered by Goedel and Turing), logic has a very modern use in verification: it serves as a robust way to specify properties of systems.

Logic in verification has three distinct important characteristics:
(1) it should be natural, a language using which a human can express correctness requirements,
(2) it should have a precise semantics, and
(3) it should be amenable to model-checking (it should be decidable and in fact efficiently tractable).

The study of logic in verification forms a very core aspect of the field, and forms the theoretical basis on which all formal methods is developed. In this course, we will study various logics that arise in this field (first-order logics, temporal logics, fixpoint logics), automata and games that serve as machine-equivalent formalisms for these logics, and algorithms that render questions on these logics tractable.

We will cover the following topics roughly: Regular languages and its logical characterizations, logics on words: MSO and FOL on words, linear-time temporal logic, logics on trees, regular tree languages, branching time temporal logics, automata on infinite words and trees, Rabin's theorem, model checking temporal logics using automata, algorithms on automata, logics on structures, fixpoint logics, games, mu-calculus and parity games, decidable logics such as reals, Pressburger arithmetic and other decidable theories, decidable logics on graphs, and combinations of decision procedures.

Mathematical maturity and some knowledge of automata theory and propositional logic required.