This course provides an introduction to some of the central ideas of formal
methods in computer science. We mainly focus on as a set of mathematical tools
for understanding complex systems, motivated by Computer-Aided Verification.
The lecture will discuss three interconnected research fields:
* Automata (on infinite words and trees)
* Logical systems (such as temporal and modal logics) for specifying operational behaviour
* Two-person games as a conceptual basis for understanding interactions between a system and its environment
This course will focus on the theoretical underpinnings, but it might also
include a small practical project.
Requirements: You need to know:
* what is a finite automaton and how the pumping lemma works,
* first-order logic,
* notions of reduction and decidability,
* some basic complexity classes (PSPACE, EXPTIME, NP).
