Automata and Formal Languages 2008/09

News | Dates | Grading | Content | Exercises | Exam | Material

This lecture requires basic knowledge in automata theory, e.g., obtained during the course 'Einführung in die theoretische Informatik'. Below there is a rough outline of the topics. This list is subject to change and will be updated based on progress and student input.

1. Finite Automata over finite words
   1. Classical constructions for DFA (union, intersection, complement, determinization)
   2. Algorithms and complexity of such constructions (e.g. PSPACE-completeness of universality of DFA)
   3. Applications: pattern matching, verification
2. Finite Automata over infinite words
   1. Omega words and omega automata
   2. Büchi automata
   3. Union, Product, Determinization, Complement
   4. Muller, Rabin, Street automata
   5. Büchi automata in verification
3. Automata and Logic
   1. Monadic Second Order Logic (MSO) over words
   2. Equivalence of MSO and regular languages
   3. Monadic Second Order logic of One successor (S1S)
   4. Equivalence of MSO and omega-regular languages
   5. Presburger arithmetic
   6. Linear Temporal Logic (LTL)
4. Timed Automata

Parts 1-3 is lectured by Javier Esparza, while part 4 is given by Jörg Kreiker.

Here is a list of the topics covered (so far):

1. Finite automata over finite words
   1. Determinization of DFA. The powerset construction. Efficient implementation of the construction.
   2. From regular expressions to NFA and back. New algorithms based on automata with RE-transitions (From RE to NFA: expansion of an initial automaton with 2 states. From NFA to RE: succesive elimination of states). Elimination algorithm for epsilon-transitions.
   3. Closure of regular languages under boolean operators. The product construction for NFAs: good for intersection, bad for union. The product construction for DFAs: good for intersection, union, difference, symmetric difference .... The product construction preserves determinism, but not minimality. Optimality of the construction.
   4. Transducers and regular relations. Product of a transducer and a NFA. Pre- and post versios of the product.
   5. Minimization of automata. Fundamental result: automaton is minimal if every state reachable and different states recognize different languages. Algorithm for checking minimality.
      Bisimulation equivalence. Definition of bisimilarity (the largest bisimulation). Bisimilarity up to k steps. Partitioning algorithm for computing the bisimilarity relation. Minimal NFA w.r.t. bisimilarity.
      Minimization of DFA automata for bounded languages. Direct computation of the minimal DFA for the intersection of two languages given as DFAs.
   6. Pattern matching. Algorithms for pattern mathing a regular expression based on NFAs and DFAs; complexiy and comparison. The case of one pattern p: minimal DFA, the overlap function, linear algorithm for computing the overlap function.
      Digresion: Two-way DFA acept regular languages.
      Verification of distributed systems. Processes as communicating automata. Asynchronous product of automata. Specifications in terms of the languages of a product. Automatic verification by checking language equality or language inclusion.
   7. Monadic Second Order Logic on Finite Words (MSO). Syntax. Intuitive semantics. Abbreviations and examples. Formal semantics. Language of a formula. Theorem: a language is regular iff it is definable in MSO.
2. Finite automata over infinite words
   1. Büchi automata (BA).
      1. Definition. Büchi acceptance condition. Examples showing that the powerset construction does not respect the recognized language. Deterministic BA are less powerful than nondeterministic BA. Omega-regular languages. A language is omega-regular iff it is recognized by a BA.
      2. Easy constructions on BA: union and intersection.
      3. Complementation of BA. Example showing that swapping final and non-final states does not work. Complementing: (1) The tree of executions of a BA on a word. (2) Ranking the tree (attaching to each node a number). (3) Automaton for the complement of the language; role played by the final states.
   2. Other automata over infinite words
      1. Muller automata. Street automata. Rabin automata. Constructions showing that all these classes recognize exactly the omega-regular languages.
   3. Monadic Second Order Logic of One Successor (S1S). Syntax. Intuitive semantics. Abbreviations and examples. Formal semantics. Language of a formula. Theorem: a language is omega-regular iff it is definable in S1S.
   4. Presburger arithmetic. Syntax. Formal semantics. Language of a formula. Theorem: Embedding of Presbuger arithmetic in S1S.
   5. Linear Temporal Logic. Syntax. Formal semantics. Language of a formula. Abbreviations. Examples. Equivalences. Algorithm transforming an LTL formula into an equivalent BA. Model-checking LTL.