Course Description

Franz Baader (Dresden), advanced, 4 hours

Automata and Logic

This course considers finite automata that work on finite or infinite words. The course concentrates on the connection between these automata and logics that play an important role in computer science, such as first-order logic, monadic second-order logic, and linear temporal logic; in particular, it will be shown how closure and decidability results for the automata can be used to obtain decidability results for these logics.


  • W. Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, pages 133-192. Elsevier Science Publishers, Amsterdam, 1990.
  • W. Thomas. Languages, automata, and logic. In G. Rozenberg and A. Salomaa, editors, Handbook of Formal Languages, volume III, pages 389-455. Springer, New York, 1997.

Markus Holzer (Giessen), introductory, 14 hours

Computational Complexity

The course on computational complexity covers the basics on sequential and parallel complexity classes. Special attention is paid to complete problems, in particular related to automata and formal language theory such as, e.g., fixed and general membership, finiteness, counting problem, etc. Moreover, the course shows deep relations between complexity classes and auxiliary space bounded automata with abstract storage.


  • C.H. Papadimitriou, Computational Complexity. Addison-Wesley, 1994
  • K.-J. Lange, Complexity and Structure in Formal Language Theory. Fundamenta Informaticae 25(3-4): 327-352, 1996
  • I.H. Sudborough, A Note on Tape-Bounded Complexity Classes and Linear Context-Free Languages. Journal of the ACM 22(4): 499-500, 1975
  • I.H. Sudborough, The Complexity of the Membership Problem for Some Extensions of Context-Free Languages. Computing Reviews 19(5): 191-215, 1976
  • D.A. Barrington, Bounded-Width Polynomial-Size Branching Programs Recognize Exactly Those Languages in NC1. Journal of Computer and System Sciences 38(1): 150-164, 1989
  • C. Damm, M. Holzer & K.-J. Lange, The Parallel Complexity of Iterated Morphisms and the Arithmetic of Small Numbers, in Proceedings of the 17th Conference on Mathematical Foundations of Computer Science, I.M. Havel & V. Koubek (eds.), Prague. Springer, LNCS 629, 1992: 227-235
  • M. Holzer, On emptiness and counting for alternating finite automata, in Developments in Language Theory II: at the Crossroads of Mathematics, Computer Science and Biology. World Scientific, 1996: 88-97
  • B. Monien, On the {LBA} Problem, in Proceedings of the International Conference Fundamentals on Computation Theory. Springer, LNCS 117, 1981: 265-280
  • B. Monien & I. Sudborough, The interface between language theory and complexity theory, in Formal Languages - Perspectives and Open Problems, R.V. Book (ed.). Academic Press, 1980: 287-324
  • M. Holzer & K.-J. Lange, On the Complexities of Linear {LL(1)} and {LR(1)} Grammars, in Proceedings of the 9th International Conference on Fundamentals of Computation Theory, Z. Ésik (ed.), Szeged. Springer, LNCS 710, 1993: 299-308
  • M. Holzer & K.-J. Lange, On the Complexity of Iterated Insertions, in New Trends in Formal Languages: Control, Cooperation, and Combinatorics. Springer, LNCS 1218, 1997: 440-453

Thierry Lecroq (Rouen), introductory, 10 hours

Text Searching and Indexing

This course will present two main basic aspects of algorithms in strings. The presented techniques can be useful in many applications including natural language processing, data compression and computational biology. More specifically the course deals with the following topics:

  • main exact single string matching algorithms (Morris-Pratt, Knuth-Morris-Pratt, Simon, Boyer-Moore Turbo-BM and Apostolico-Giancarlo algorithms);
  • main indexing structures and the algorithms for building them (suffix trees, compact suffix trees, suffix automata, compact suffix automata, suffix arrays and enhanced suffix arrays).

Rupak Majumdar (Kaiserslautern), introductory, 10 hours

Software Model Checking

The last ten years have seen a lot of interesting tools that can automatically analyze properties of software implementations. In this series of lectures, we shall study the technical developments behind these tools. The lectures will cover the basic principles of symbolic model checking and abstraction, and show how ideas like predicate abstraction, counterexample-guided refinement, interpolation, and concolic execution can be used together to build sophisticated program analysis tools.


  • Ranjit Jhala and Rupak Majumdar. Software Model Checking. ACM Computing Surveys, 2009.

Bernhard Steffen (Dortmund), introductory/advanced, 18 hours

Automata Learning from Theory to Application

  1. Introduction to automata learning (the essence) (2h lecture, 2h tutorial)
    The focus here will be on 'active' automata learning in the sense of Angluin's L* algorithm.
    Besides the foundations in terms of classical automata theory, enough information will be provided to prepare for the lab-based tutorial session for providing a first tangible experience of the technology, its strength and its weaknesses, e.g. concerning the roles of the oracles and the treatment of counter examples.
    The lab-session will also introduce the LearnLib (, which will be used throughout the course to illustrate phenomena, and the impact on certain methods and algorithms.
  2. Enhancements (2h lecture, 2h tutorial)
    The focus here will be on totally application-independent enhancement concerning:
    • the use of data structures,
    • the efficient treatment of counter examples,
    • the efficient realization of equivalence queries,
    • other automata models (e.g. Mealy machines, IO-Automata).
    For illustration we will use the scenario set up for the ZULU challenge ( during the lab-based tutorial session.
  3. Learning in practice (2h lecture, 4h hands on session)
    This lecture will focus on the application aspect of learning, addressing various scenarios (cf RERS: Besides some technical aspects, like resetting and remote testing, this lecture will focus on abstraction, the central notion for bringing learning to practical use: on the one hand, automata learning is too expensive to apply directly to most realistic concrete systems; on the other hand, smoothly dealing with abstraction without having to build a detailed concrete model is one of the major 'selling points' of automata learning.
    The lab-based tutorial session will guide through the development of a learning setup for a real life application, comprising most of the addressed problems and phenomena.
  4. Advanced techniques (2h lecture, 2h tutorial)
    This final session will summarize the essence of the course in a way that highlights ongoing work, perspectives, and open problems. The lab-based tutorial session will present the RERS-Challenge 2011, which will be held in Vienna in October 2011. In particular, it will support students to have a jump start for this challenge, which will also provide a "best student solution" award.

    References: Please see the links above.

    Wolfgang Thomas (Aachen), introductory/advanced, 6 hours

    omega-Automata and Infinite Games

    We give a short introduction to automata over infinite strings (and the associated class of "regular omega-languages") and then focus on a self-contained solution of the fundamental theorem on regular infinite games, the "Buechi-Landweber Theorem" (1969).

    It shows how to decide who (of the two players) wins a regular infinite game, and how to construct a finite-state winning strategy for the winner. In modern terms, this solves the controller symthesis problem for regular specifications. The given proof is a result of decades of work in polishing the theory. The last part of the tutorial is devoted to an overview of recent developments, including context-free specifications and aspects of optimization.


    • W. Thomas. Church's problem and a tour through automata theory. In A. Avron, N. Dershowitz, and A. Rabinovich, editors, Pillars of Computer Science, Essays Dedicated to Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday, volume 4800. Springer, 2008, pages 635-655.

    Sheng Yu (London ON), introductory/advanced, 8 hours

    Finite Automata and Regular Languages

    Three basic models of finite automata, Deterministic Finite Automaton (DFA), Nondeterministic Finite Automaton (NFA), and Alternating Finite Automaton (AFA), will be reviewed. Their relationships with regular expressions and derivatives will be introduced.

    We will study the basic concept of cover automata for finite languages and several algorithms for constructing a minimal cover automaton from a given finite language. The state complexity of regular languages will also be studied. The basic concept and motivations will be introduced. A number of results on the state complexity of individual operations and combined operations will be studied.


    • J. Hopcroft, R. Motwani, and J.D. Ullman, Introduction to Automata Theory,' Languages, and Computation, 3rd Edition, Addison Wesley 2007.
    • S. Yu, "Chapter 2: Regular Languages", in G. Rozenberg and A Salomaa edited Handbook of Formal Languages, Springer 1998, pp. 41-110.
    • C. Campeanu, N. Santean, and S. Yu, "Minimal Cover-Automata for Finite Languages" in Theoretical Computer Science 267 (2001) 3-16.
    • S. Yu, Q. Zhuang, and K. Salomaa, "On the State Complexity of Some Basic Operations on Regular Languages", in Theoretical Computer Science 125 (1994) 315-328.
    • A. Salomaa, K. Salomaa, and S. Yu, "State Complexity of Combined Operations", Theoretical Computer Science 383 (2007) 140-152.