| Kurzkommentar |
Overview
Automata-based methods are crucial components for many areas of computer science, e.g. for logic, program analysis, verification, and semantic analysis of data. This is reflected in several lectures at Saarland University which make regular use of automata theory, in particular Automata, Games and Verification, Data Networks II/Verification II, and Database Theory. With this seminar, I want to bridge the gap and highlight connections and synergies between the existing automata-based lectures, and provide the students with a flexible set of automata-based tools to rely on in the future.
The only entrance requirement is a basic knowledge about finite word automata, decidability and complexity, as demonstrated e.g. by a successful participation in the lecture Grundzüge der Theoretischen Informatik. The contents of the related core lecture Verification as well as the above-mentioned in-depth lectures will also definitely be helpful.
Entrance requirements: Grundzüge der Theoretischen Informatik
Assessment/Exams: Contributions to discussions; talk; written elaboration; final oral exam on the whole content of the seminar
Contents and Competences
I will initially create a common ground for all participants by introducing the basics of finite tree automata with and without constraints, DAG automata, timed automata and hybrid automata, after which the students take over. The focus in the talks presented by students will be on developing decision procedures or undecidability proofs and applying them to reasoning in logic and to verification problems.
Soft competences to be developed: Students can analyze and evaluate scientific articles, present and discuss scientific work orally and in writing, evaluate talks, and give constructive feedback.
Hard competences to be developed: Students can model abstract problems elegantly using various forms of automata. In particular, they know how to decide properties of tree, DAG, timed and hybrid automata and can apply such automata to practical problems from logic and verification.
In more detail, we will treat the following subjects:
• Advanced topics on finite automata: Minimization and efficient, polynomial learning of minimal automata.
• As an introduction into more complex automata models: Finite tree automata (top-down, bottom-up, nondeterministic and deterministic) with their closure properties and decidability results; regular tree languages and the corresponding pumping lemma; application to the theory of free function symbols.
• Finite tree automata with equality constraints, which relate to reasoning modulo equational theories and which demonstrate a very fine line between (efficient) decidability and undecidability.
• DAG automata, which work on directed acyclic graphs, and their application in unification.
• Timed and hybrid automata, with an emphasis on decidability and the application to verification tasks.
About the lecturer Matthias Horbach
2005 Diplom in Mathematics from Saarland University
2006 Diplom in Informatics from Saarland University
2010 Ph.D. (Dr. rer. nat.) at Saarland University and Max Planck Institute for Informatics
2011-12 Researcher at University of New Mexico (Albuquerque, USA) on a DAAD postdoc grant
currently Researcher at MPI-I and Koblenz University in the DFG-Projekt AVACS |
