Wolfgang Thomas holds the Francqui Chair 2012-2013 at the Department of Computer Science, Faculty of Sciences, UMONS.
Wolfgang Thomas is Full Professor of Computer Science at RWTH Aachen (Germany). His main research interest is the development of
automata theory as a framework for modeling, analyzing, verifying and synthesizing systems.
Logic and Automata: Fundamentals and Perspectives
Inaugural lecture at building "Centre Vésale" (Room 20) Thursday, April 18, 2013
In this opening lecture, we give a historical account of the interplay between the concepts of "algorithm", "logic", and "automaton" which are ubiquitous today in computer science. In the first part it is shown how a clear understanding of "algorithm" developed in a process of several centuries via an integration of arithmetic and logic. In the second part we recall how automata theory entered within computer science as a catalyst for doing logic algorithmically: Not only are automata a powerful framework for modeling systems, but also they are pivotal in devising procedures that solve problems involving formal logic, for example in the automated verification and synthesis of programs. Starting from this, we outline the course of the subsequent lectures and discuss some long-term challenges. [17:00-17:30] Welcome [17:30-19:00] Logic, Algorithms, and Automata: A Historical Journey [slides] [19:00] Reception Francqui lecture series at building "Centre Vésale" (Room 25) Friday, April 26, 2013: Monadic Theories
The idea of these four lectures is to give an intuitive but nevertheless fairly self-contained account of the celebrated connection between monadic second-order logic and finite automata, also termed "a match made in heaven" (Moshe Vardi). The aim is to develop a general understanding of when the model-checking problem for an infinite-state structure is decidable (w.r.t. to monadic second-order logic). We start with an exposition of the central Results of the Golden 1960’s, concerning automata on infinite words and infinite trees. In the second lecture, on Prefix Rewriting and the Pushdown Hierarchy, we explain strong decidability results on infinite models that are "tree-like"; these models arise from the infinite binary tree by applying the two fundamental operations of "interpretation" and "unfolding". In the third part, titled The Composition Method, we explain a purely logical framework that generalizes the automata-theoretic method and can be used to obtain decidability results where automata are no more suitable. In the final lecture, Undecidability Results, we treat different ways in which second-order theories can turn out undecidable, based on different connections to first-order arithmetic. [10:00-11:00] Results of the Golden 1960’s Revisited [slides] [11:00-11:30] Coffee Break [11:30-12:30] Prefix Rewriting and the Pushdown Hierarchy [slides] [12:30-14:00] Lunch [14:00-15:00] The Composition Method [slides] [15:00-15:30] Coffee Break [15:30-16:30] Undecidability Results [slides] Friday, May 3, 2013: Games
Infinite two-person games with complete information are a simple model for the study of non-terminating reactive systems. It has been extended in a great variety of directions (concurrent, stochastic, multi-player games, and many more). However, in the present four lectures we stay with the basic model, starting in the first lecture with an exposition of the Fundamental Results on Infinite Two-Person Games, and then presenting recent results, some of them obtained in the group of the speaker, that hopefully refine the understanding of these games. In the second lecture Strategies in a Logical Setting we pursue the question in which way "simple winning conditions" allow for "simple winning strategies". In the third lecture Concepts of Strategy we discuss different formats for the specification of winning strategies and also address generalized formats of strategy (where a player may decide on his moves after a delay). In the final lecture Winning Infinite Games in Finite Time we take up ideas of McNaughton on the decision of the winner of an infinite game after a finite number of moves; recent results on this approach open a new approach to the construction of winning strategies.
[10:00-11:00] The Fundamental Results on Infinite Two-Person Games [slides] [11:00-11:30] Coffee Break [11:30-12:30] Strategies in a Logical Setting [slides] [12:30-14:00] Lunch [14:00-15:00] Concepts of Strategy [slides] [15:00-15:30] Coffee Break [15:30-16:30] Winning Infinite Games in Finite Time [slides]