Differences
This shows you the differences between two versions of the page.
| Next revision | Previous revision | ||
|
lat1 [2009/09/18 12:47] vkuncak created |
lat1 [2009/09/18 12:48] (current) vkuncak |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| - | ====== Logic and Automata Theory ====== | + | ====== Doctoral Course: Logic and Automata Theory ====== |
| - | ====== Introductory Lecture: Today 1pm-2pm in BC 355 ====== | + | **4 credits** |
| - | A course in the [[http://phd.epfl.ch/edic|EPFL Doctoral Program in Computer and Communication Sciences]] | + | **In the course, you will learn how specify and verify properties that |
| + | give formal meaning to words such as 'eventually' and 'until' and how to | ||
| + | automatically verify that systems satisfy such properties. You will | ||
| + | learn about more general types of finite state machines: machines run | ||
| + | continuously, such as a web server, and machines that accept not only | ||
| + | words (strings) but also trees (tree automata). You will learn about | ||
| + | some of the widely used results such as decision procedures for linear | ||
| + | integer arithmetic, and some classic deep results such as the decision | ||
| + | procedure for monadic second-order logic over (possibly infinite) trees. | ||
| + | You will also see how these results can be applied to verification, but | ||
| + | also synthesis of systems that are correct by construction.** | ||
| - | **4 credits** | + | ====== Introductory Lecture: Today 1pm-2pm in BC 355 ====== |
| **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. | **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 Mu-calculus, a widely used tool for specification and verification of systems. | ||
| - | - Logical theory of integer arithmetic. Decidability results using both quantifier elimination and automata theory. Cobham's base dependence theorem. | ||
| **Schedule**: (lectures and exercises): Fridays 13:15-16:00 | **Schedule**: (lectures and exercises): Fridays 13:15-16:00 | ||