Teaching

Advanced Logic

In the early 60s, Büchi, Elgot and Trakhtenbrot formulated a correspondence between regular finite word languages and those described by weak second-order monadic logic. Beside the nice mathematical theory, this correspondence has several applications. An example of application is a family of decision procedures for some logical formalisms that are particularly useful for system specifications. Another example is a method to synthesize a constant space algorithm from a problem specification.

The Büchi-Elgot-Trakhtenbrot correspondence extends to infinite words and monadic second order logic. It also extends to the languages of finite and infinite trees, allowing to completely automate reasoning for many useful logics in checking programs such as Presburger arithmetic, LTL, CTL, CTL* temporal logics, modal mu-calculus, etc.

The purpose of this course is to discover some of the simplest of these correspondences between automata and logics in a rather practical approach. Along with the nice theory, you will experiment concretely with the MONA tool and you will have to work out two rather guided programming assignments.

Moodle password: ILoveAL25!