Logic and languages

This course introduces the logic of finite models, such as words, trees and finite graphs, as well as temporal logics used in verification. We will also introduce description logics, which are used to formally represent knowledge in a particular domain (e.g. medicine) to improve querying and information sharing. We'll look at the expressive power of the logics under consideration, as well as various algorithmic problems (formula validation on a model, formula satisfiability, logical inference, etc.).

We'll also look at learning LTL automata and formulas from examples in both passive and active contexts. We will discuss algorithms associated with these problems (upper bounds) as well as complexity issues (lower bounds). Time permitting, we will also highlight a close link between automata theory and the complexity of algebraic circuits, and show how results from one can be applied to the other.