Difference between revisions of "Lat18"

Revision as of 19:55, 16 September 2018

Logic and Automata Theory

Lecturer: Radu_Iosif

Objectives: Many major hardware (Intel, IBM) and software (Microsoft) companies are now using the technique of Model Checking in practice. Examples of its use include the verification of VLSI circuits, communication protocols, software device drivers, real-time embedded systems, and security algorithms. The works of A. Pnueli, E. Clarke, E.A Emerson and J. Sifakis on algorithmic verification of systems using the Model Checking has been awarded the 1996 and 2007 Turing awards. The basis of this work is the relation of logic with automata theory, which was introduced by the seminal works of Buechi (1960) and Rabin (1969). This course is intended to introduce the student to these techniques, focusing on decision methods for classical non-interpreted logics and integer arithmetic theories.

Syllabus:

• Classical first- and second-order logic, finite word and tree automata, closure properties and language emptiness.
• Relationship between Weak Monadic Second-Order Logic and finite automata.
• Infinite automata on words (Buechi, Mueller) and on trees (Rabin) automata, and their relationship with Monadic Second-Order Logic.
• Game theory. Proof of Rabin's Complementation Theorem. Application of game theory to logic.
• Logical theory of integer arithmetic. Decidability results using both quantifier elimination and automata theory.

Prerequisites: basic notions of boolean logic

Level: PhD and Master 2

Schedule: 3 hours per week during 8 weeks (24 hrs)

Location: IMAG building on University Grenoble Campus

Register:

• send email to Radu.Iosif@univ-grenoble-alpes.fr indicating your name and year of Phd/Master program
• for PhD students, indicate also your host laboratory and name of your PhD advisor

Past LAT courses