The spring school consists in nine lectures presenting important developments in language theory, automata, and games.

The schedule is available there.

This lecture presents bridges between logical and algebraic descriptions of classes of regular languages of finite words. We show how to use such correspondences to derive expressiveness results, and algorithms to decide whether a given language is expressible in a given formalism. The lecture will review several such classes and describe a general framework unifying these results.

- Pin, Jean-Eric, Syntactic semigroups. Handbook of formal languages, G. Rozenberg, A. Salomaa (eds.) vol 1, pp. 679--746, Springer 1997.
- Pascal Tesson and Denis Thérien, Logic Meets Algebra: the Case of Regular Languages, Logical Methods in Computer Science 3(1), 2007
- V. Diekert, P. Gastin, M. Kufleitner, A Survey on Small Fragments of First-Order Logic Over Finite Words, International Journal of Foundations of Computer Science (IJFCS) 19(3), pp 513=548, 2008
- T. Wilke, Classifying discrete temporal properties, STACS'99, LNCS, pp 32-46
- V. Diekert, P. Gastin, Paul, First-order definable languages, in Logic and Automata: History and Perspectives, J. Flum, E. Graedel, and T. Wilke (Eds.), Texts in Logic and Games vol 2., pp. 261-306, Amsterdam University Press, 2008

Stochastic pushdown games are infinite-state turn-based stochastic games where the states are pushdown configurations and possible moves are determined by a finite set of prefix-rewriting rules. The existing results about stochastic pushdown games concern mainly termination and reachability objectives. In the lecture we give an overview of these results and the associated proof techniques. A special attention is devoted to explaining the difference between finite-state and infinite-state games

- T. Brázdil, V. Brožek, A. Kučera, and J. Obdržálek. Qualitative Reachability in Stochastic BPA Games. To appear in Information and Computation. Elsevier, 2011. A preprint available at http://www.fi.muni.cz/usr/kucera/papers/IC2011.pdf
- K. Etessami and M. Yannakakis, Efficient Qualitative Analysis of classes of Recursive Markov Decision Processes and Simple Stochastic Games. Proc. of STACS 2006, Springer. A preprint of a journal version available at http://homepages.inf.ed.ac.uk/kousha/j_sub_rmdp_rssg.pdf
- A. Kučera. Turn-Based Stochastic Games. In Lectures in Game Theory for Computer Scientists (edited by Krzysztof R. Apt and Erich Grädel). Pages 146-184, Cambridge University Press, 2011.

The objective of this lecture will be to explain and to give examples and applications of the following result: "A set of regular languages is a lattice of languages if and only if it can be defined by a set of profinite equations". Connections with Ehreufeuch-Fraïssé games will also be given.

- M. Gehrke, S. Grigorieff, J.-E. Pin, A topological approach to recognition, ICALP 2010, Part II, Lecture Notes in Computer Science 6199, Springer Verlag, (2010), 151-162.
- M. Gehrke, S. Grigorieff, J.-E. Pin, Duality and equational theory of regular languages, ICALP 2008, Part II, Lecture Notes in Computer Science 5126, Springer Verlag, (2008), 246-257.
- J.-E. Pin, Profinite methods in automata theory, 26th International Symposium on Theoretical Aspects of Computer Science (STACS 2009), Susanne Albers and Jean-Yves Marion, eds. Internationales Begegnungs- Und Forschungszentrum für Informatik (IBFI), Schloss Dagstuhl, Dagstuhl, Germany, 2009, 31-50.

Finite state machines and automata [1] are the subject of the very rich theory of regular languages. Those formalisms are relevant at a theoretical level, as well as for their applications, such as in verification. It is clear from the origin that an similar theory that would have quantitive capapabilities would be of great interest. A general framework for such an extension has been proposed by Schützenberger [2] yieding the so called weighted automata. It gives a very appealing algebraic presentation, but usually yields to undecidability for most interesting problems.

In this lecture we will consider the problem of extending automata with counting capabilities, with a particular attention to the model of distance automata of Hashiguchi [3] and their extensions [4] and [5,6]. Those models of automata retain part of the nice theory of regular languages, in particular concerning decidability, and have at the same time counting features.

- [1] Michael O. Rabin and Dana Scott, Finite automata and their decision problems, IBM J. Res. and Develop. 3:114–125, 1959.
- [2] Marcel-Paul Schützenberger, On the definition of a family of automata, Information and Control 4:245–270, 1961.
- [3] Kosaburo Hashiguchi. Limitedness theorem on finite automata with distance functions. J. Comput. Syst. Sci., 24(2):233-244, 1982.
- [4] Daniel Kirsten. Distance desert automata and the star height problem. RAIRO, 3(39):455-509, 2005.
- [5] Mikolaj Bojanczyk and Thomas Colcombet. Bounds in omega-regularity. Logical Methods in Computer Science, 2009. To appear.
- |6] Thomas Colcombet. Regular cost functions, Part I: logic and algebra over words. Submitted.

Automatic structures were introduced by Khoussainov and Nerode in 1994. Roughly speaking, a relational structure is automatic, if the elements of the structure can be coded by words in such a way that the universe is a regular language and every relation of the structure can be recognized by a synchronous multi-tape automaton. The main motivation for studying automatic structures is the fundamental fact that every automatic structure has a decidable first-order theory. In recent years, a rich theory of automatic structures started to develop, which contains both structural and more algorithmic results.

In the two talks, I will present a survey on the algorithmic theory of automatic structures. In the first lecture, we will consider decidable logics for automatic structures and their complexity. We will outline the standard automata theoretic decision algorithm for the first-order theory of an automatic structure as well as generalizations for richer logics. More efficient (elementary) algorithms for subclasses of automatic structures (e.g. automatic structures of bounded degree) will be mentioned too. The second lecture will survey recent results for the isomorphism problem for classes of automatic structures. For instance, we will show that already for automatic equivalence relations, the isomorphism problem is undecidable.

Further details can be found in the following two papers:

- Dietrich Kuske and Markus Lohrey Automatic structures of bounded degree revisited to appear in Journal of Symbolic Logic
- Dietrich Kuske and Markus Lohrey The isomorphism problem on classes of automatic structures Proceedings of LICS 2010, pp. 160-169

Stochastic games are a mathematical model of competition over discrete time. The existence and computability of the values of stochastic games is a central algorithmic question.

The lecture will present a few algorithms to compute efficiently the values of stochastic games as well as optimal or epsilon-optimal strategies for both players. The complexity of such a task depends on the class of stochastic games considered, ranging from Markov chains to Markov decision processes and two-player stochastic games, and from perfect-information stochastic games to repeated games with imperfect information.

- Anne Condon. The complexity of stochastic games. Information and Computation, 96:203–224, 1992.
- A.J. Hoffman and R. M. Karp, On Nonterminating Stochastic Games, Management Science, Vol. 12, No. 5, January 1966, pp. 359-370.
- J.F. Mertens and A. Neyman, Stochastic Games, International Journal of Game Theory, 10, 1981, 53-66.
- Martin L. Puterman, Markov Decision Processes, Wiley, 2005.
- Lloyd Shapley, Stochastic Games, Proceedings Of the National Academy of Science of the USA, 1953, pp. 1095-1100.
- Sylvain Sorin. A First Course On Zero-Sum Repeated Games, Springer-Verlag, 2002.
- Stephen J. Wright, Primal-Dual Interior-Point Methods, Siam,1997.

The theory of finite monoids/semigroups has been a very successful tool for understanding regular languages of words. Two important applications are: understanding the expressive power of different logics on words, such as first-order logic, and string algorithms.

In my talk, I will describe the progress that has been made for tree
languages. Many of the important problems remain open. In particular,
it is not known if the following decision problem is decidable:

INPUT: a regular tree language, given e.g. by a tree automaton.

QUESTION: is the regular tree language definable in first-order logic?

Nevertheless, some simpler logics have been understood, and also some of the algebra is mature enough to be used in pattern matching algorithms, especially in XML. I will present some of these results, including:

- Why are there so many kinds of algebras for trees?
- An effective characterization of a simple logic, namely EF.
- An application of forest algebra to incremental evaluation of regular tree languages.

No particular knowledge of topology is required. We will start from scratch with finite and infinite 2-player games with perfect information (no chance, nothing hidden). We will look into the various usual ways people play (they alternate, they pass their turns, they play several moves in a row, they even undo their previous moves...). From these game-like behaviors, we will derive the basic the topological notions. From there we will concentrate on games played on graphs, relate this to the general picture, and explain in details the implications of determinacy, and its bizarre relationship with choice.

In a second step we will use both games and topology to discuss the complexity of many omega-languages recognized essentially by automata (Büchi automata, counter automata, pushdown automata, alternating automata, tree automata, etc). As a starter we will present the Wagner hierarchy of omega-regular languages, then move on to the general Wadge hierarchy: the classification method that is the finest. We will give an overview of the many results on the Wadge complexity of omega-languages, together with the even more numerous open questions. If time permits, we will show (following a result from Arnold and Niwinski) how Wadge considerably helps proving the strictness of the semantical mu-calculus hierarchy (by simply playing a game where deciding the winner requires other games to be settled).