M2 Course Proposal, ENS-Lyon Short Description: Prerequisites: ideally the students need to have some basic knowledge on standard finite automata and regular languages. We will anyway provide some notes during the course to refresh these notions. The students are also supposed to have already been exposed to (first order and propositional) logic, be familiar with the meaning of the usual connectives (and, or, not, exists, forall).