Infinite games are studied in a format where two players, called Player 1 and Player 2, generate a play by building up an omega-word as they choose letters in turn. A game is specified by the omega-language which contains the plays won by Player 2. We analyze omega-languages generated from certain classes K of regular languages of finite words (called *-languages), using natural transformations of *-languages into omega-languages. Winning strategies for infinite games can be represented again in terms of *-languages. Continuing work of Selivanov (2007) and Rabinovich et al. (2007), we analyze how these strategy *-languages are related to the original language class K. In contrast to that work, we exhibit classes K where strategy representations strictly exceed K.

A game-theoretic model for the study of dynamic networks is proposed and analyzed. The model is motivated by communication networks that are subject to failure of nodes and where the restoration needs resources. The corresponding two-player game is played between ``Destructor'' (who can delete nodes) and ``Constructor'' (who can restore or even create nodes under certain conditions). We also include the feature of information flow by allowing Constructor to change labels of adjacent nodes. As an objective for Constructor the network property to be connected is considered, either as a safety condition or as a reachability condition (in the latter case starting from a non-connected network). We show under which conditions the solvability of the corresponding games for Constructor is decidable, and in this case obtain upper and lower complexity bounds, as well as algorithms derived from winning strategies. Due to the asymmetry between the players, safety and reachability objectives are not dual to each other and are treated separately.

Infinite games are studied in a format where two players, called Player 1 and Player 2, generate a play by building up an omega-word as they choose letters in turn. A game is specified by the omega-language which contains the plays won by Player 2. We analyze omega-languages generated from certain classes K of regular languages of finite words (called *-languages), using natural transformations of *-languages into omega-languages. Winning strategies for infinite games can be represented again in terms of *-languages. Continuing work of Selivanov (2007) and Rabinovich et al. (2007), we analyze how these strategy *-languages are related to the original language class K. In contrast to that work, we exhibit classes K where strategy representations strictly exceed K.

In model-checking, systems are often given as products. We propose an approach that is built on a preprocessing of specifications in terms of appropriate automata. This allows to incorporate information about the local behaviour and synchronization of the system components into the specification. We develop a framework of (partially) synchronized automaton products and a format of corresponding specification automata that allows for a compositional failure detection of linear regular properties (either for finite or for infinite behaviour). As a result we obtain an algorithm which separates the local and the non-local segments of system runs, resulting in improved complexity bounds in typical specifications.

In model-checking, systems are often given as products. We propose an approach that is built on a preprocessing of specifications in terms of appropriate automata. This allows to incorporate information about the local behaviour and synchronization of the system components into the specification. We develop a framework of (partially) synchronized automaton products and a format of corresponding specification automata that allows for a compositional failure detection of linear regular properties (either for finite or for infinite behaviour). As a result we obtain an algorithm which separates the local and the non-local segments of system runs, resulting in improved complexity bounds in typical specifications.

A game-theoretic model for the study of dynamic networks is analyzed. The model is motivated by communication networks that are subject to failure of nodes and where the restoration needs resources. The corresponding two-player game is played between ``Destructor'' (who can delete nodes) and ``Constructor'' (who can restore or even create nodes under certain conditions). We also include the feature of information flow by allowing Constructor to change labels of adjacent nodes. As objective for Constructor the network property to be connected is considered, either as a safety condition or as a reachability condition (in the latter case starting from a non-connected network). We show under which conditions the solvability of the corresponding games for Constructor is decidable, and in this case obtain upper and lower complexity bounds, as well as algorithms derived from winning strategies. Due to the asymmetry between the players, safety and reachability objectives are not dual to each other and are treated separately.

We provide decidability and undecidability results on the model-checking problem for infinite tree structures. These tree structures are built from sequences of elements of infinite relational structures. More precisely, we deal with the tree iteration of a relational structure M in the sense of Shelah- Stupp. In contrast to classical results, where model-checking is shown decidable for MSO-logic, we show decidability of the tree model-checking problem for logics that allow only path quantifiers and chain quantifiers (where chains are subsets of paths), as they appear in branching time logics; however, at the same time, the tree is enriched by the equal-level relation (which holds between vertices u, v if they are on the same tree level). We separate cleanly the tree logic from the logic used for expressing properties of the underlying structure M. We illustrate the scope of the decidability results by showing that two slight extensions of the framework lead to undecidability. In particular, this applies to the (stronger) tree iteration in the sense of Muchnik-Walukiewicz.

The problem of solvability of infinite games is closely connected with the classical question of uniformization of relations by functions of a given class. We work out this connection and discuss recent results on infinite games that are motivated by the uniformization problem.

In Bollue et al. (2009), a methodology was introduced for the synthesis of behavioral controllers for discrete-event systems. The approach is based on NCES-like Petri net models of the uncontrolled plant and additional goal and safety specifications given by linear marking constraints. This paper presents different approaches to improve the synthesis process with respect to efficiency and applicability. One focus is the use of satisfiability checking of systems of integer linear inequations in the preprocessing of the model for the elimination of unnecessary complexity during the process. Further, several improvements of the synthesis algorithm itself are discussed, which increase the efficiency by applying an advanced guided search and by reusing already found partial solutions.

We present a game-theoretic framework for modeling and solving routing problems in dynamically changing networks. The model covers the aspects of reactivity and non-termination, and it is motivated by quality-of-service provisioning in cognitive radio networks where data transmissions are interfered by primary systems. More precisely, we propose an infinite two-player game where a routing agent has to deliver network packets to their destinations while an adversary produces demands by generating packets and blocking connections. We obtain results on the status of basic problems, by showing principal limitations to solvability of routing requirements and singling out cases with algorithmic solutions.

We study variants of regular infinite games where the strict alternation of moves between the two players is subject to modifications. The second player may postpone a move for a finite number of steps, or, in other words, exploit in his strategy some lookahead on the moves of the opponent. This captures situations in distributed systems, e.g. when buffers are present in communication or when signal transmission between components is deferred. We distinguish strategies with different degrees of lookahead, among them being the continuous and the bounded lookahead strategies. In the first case the lookahead is of finite possibly unbounded size, whereas in the second case it is of bounded size. We show that for regular infinite games the solvability by continuous strategies is decidable, and that a continuous strategy can always be reduced to one of bounded lookahead. Moreover, this lookahead is at most doubly exponential in the size of the parity automaton recognizing the winning condition. We also show that the result fails for non-regular games where the winning condition is given by a context-free omega-language.

We analyze a model of fault-tolerant systems in a probabilistic setting, exemplified by a simple routing problem in networks. We introduce a randomized variant of a model called the ``sabotage game'', where an agent, called ``Runner'', and a probabilistic adversary, ``Nature'', act in alternation. Runner generates a path from a given start vertex of the network, traversing one edge in each move, while after each move of Runner, Nature deletes some edge of the current network (each edge with the same probability). Runner wins if the generated finite path satisfies a ``winning condition'', namely that a vertex of some predefined target set is reached, or - more generally - that the generated path satisfies a given formula of the temporal logic LTL. We determine the complexity of these games by showing that for any probability p and epsilon>0, the following problem is PSPACE-complete: Given a network, a start vertex u, and a set F of target vertices (resp. an LTL formula phi), and also a probability p' in [p-epsilon,p+epsilon], is there a strategy for Runner to reach F (resp. to satisfy phi) with a probability >= p'? This PSPACE-completeness establishes the same complexity as was known for the non-randomized sabotage games (by the work of Löding and Rohde), and it sharpens the PSPACE-completeness of Papadimitriou's ``dynamic graph reliability'' (where probabilities of edge failures may depend on both the edges and positions of Runner). Thus, the ``coarse'' randomized setting, even with uniform distributions, gives no advantage in terms of complexity over the non-randomized case.

Pioneers of logic, among them J.R. Büchi, M.O. Rabin, S. Shelah, and Y. Gurevich, have shown that monadic second-order logic offers a rich landscape of interesting decidable theories. Prominent examples are the monadic theory of the successor structure S₁ = (N, +1) of the natural numbers and the monadic theory of the binary tree, i.e., of the two-successor structure S₂ = ({0, 1}^*, · 0, · 1). We consider expansions of these structures by a monadic predicate P. It is known that the monadic theory of (S₁, P) is decidable iff the weak monadic theory is, and that for recursive P this theory is in Delta₃⁰, i.e. of low degree in the arithmetical hierarchy. We show that there are structures (S₂, P) for which the first result fails, and that there is a recursive P such that the monadic theory of (S₂, P) is Pi₁¹ -hard.

This paper presents an approach to the synthesis of behavioral controllers for Discrete Event Systems given a Petri net based plant model and linear safety and goal constraints. First, the model of the uncontrolled plant is converted into a set of so called unified transitions, which have linear constraints on the net marking as preconditions and a change of marking as firing effect. Based on this set, an algorithm is presented to find paths from a given start marking or a set of start markings to markings fulfilling the goal constraints, while staying within a feasible marking set given by linear safety constraints. The presented algorithm makes use of characteristics typically found in plant models to perform a guided search for feasible paths and thereby significantly improves efficiency in comparison to computing the whole reachability graph.

In model-checking the systems under investigation often arise in the form of products. The compositional method, developed by Feferman and Vaught in 1959, fits to this situa- tion and can be used to deduce the truth of a formula in the product from information in the factors. Building on earlier work of Wöhrle and Thomas (2004), we study first-order logic with reachability predicates over finitely synchronized products (i.e. synchronized products with a finite number of synchronization transitions). We extend the reachability predicates by conditions on the length of the corresponding paths, formulated in Pres- burger arithmetic. For finitely synchronized products with these enhanced reachability predicates we prove a composition theorem and then show that severe limitations exist for generalisations of this result.

Given a set P of natural numbers, we consider infinite games where the winning condition is a regular omega-language parametrized by P. In this context, an omega-word, representing a play, has letters consisting of three components: The first is a bit indicating membership of the current position in P, and the other two components are the letters contributed by the two players. Extending recent work of Rabinovich we study here predicates P where the structure (N, +1, P) belongs to the pushdown hierarchy (or ``Caucal hierarchy''). For such a predicate P where (N, +1, P) occurs in the k-th level of the hierarchy, we provide an effective determinacy result and show that winning strategies can be implemented by deterministic level-k pushdown automata.

Given a set P of natural numbers, we consider infinite games where the winning condition is a regular omega-language parametrized by P. In this context, an omega-word, representing a play, has letters consisting of three components: The first is a bit indicating membership of the current position in P, and the other two components are the letters contributed by the two players. Extending recent work of Rabinovich we study here predicates P where the structure (N, +1, P) belongs to the pushdown hierarchy (or ``Caucal hierarchy''). For such a predicate P where (N, +1, P) occurs in the k-th level of the hierarchy, we provide an effective determinacy result and show that winning strategies can be implemented by deterministic level-k pushdown automata.

We analyze a model of fault-tolerant systems in a probabilistic setting. The model has been introduced under the name of ``sabotage games''. A reachability problem over graphs is considered, where a ``Runner'' starts from a vertex u and seeks to reach some vertex in a target set F while, after each move, the adversary ``Blocker'' deletes one edge. Extending work by Löding and Rohde (who showed PSPACE-completeness of this reachability problem), we consider the randomized case (a ``game against nature'') in which the deleted edges are chosen at random, each existing edge with the same probability. In this much weaker model, we show that, for any probability p and epsilon>0, the following problem is again PSPACE-complete: Given a game graph with u and F and a probability p' in the interval [p-epsilon,p+epsilon], is there a strategy for Runner to reach F with probability >= p'? Our result extends the PSPACE-completeness of Papadimitriou's ``dynamic graph reliability''; there, the probabilities of edge failures may depend both on the edge and on the current position of Runner.

We survey classical and selected recent work on the reachability problem over finitely presented infinite graphs. The problem has a history of 100 years, and it is central for automatic verification of infinite-state systems. Our focus is on graphs that are presented in terms of word or tree rewriting systems.

Over trees and partial orders, chain logic and path logic are systems of monadic second-order logic in which second-order quantification is applied to paths and to chains (i.e., subsets of paths), respectively; accordingly we speak of the path theory and the chain theory of a structure. We present some known and some new results on decidability of the path theory and chain theory of structures that are enhanced by features of synchronization between paths. We start with the infinite two-dimensional grid for which the finite-path theory is shown to be undecidable. Then we consider the infinite binary tree expanded by the binary ``equal level predicate'' E. We recall the (known) decidability of the chain theory of a regular tree with the predicate E and observe that this does not extend to algebraic trees. Finally, we study refined models in which the time axis (represented by the sequence of tree levels) or the tree levels themselves are supplied with additional structure.

In this essay we discuss the origin, central results, and some perspectives of algorithmic synthesis of nonterminating reactive programs. We recall the fundamental questions raised more than 50 years ago in ``Church's Synthesis Problem'' that led to the foundation of the algorithmic theory of infinite games. We outline the methodology developed in more recent years for solving such games and address related automata theoretic problems that are still unresolved.

We show the solvability of an optimization problem on infinite two-player games. The winning conditions are of the ``request-response'' format, i.e. conjunctions of conditions of the form ``if a state with property Q is visited, then later also a state with property P is visited''. We ask for solutions that do not only guarantee the satisfaction of such conditions but also minimal wait times between visits to Q-states and subsequent visits to P-states. We present a natural class of valuations of infinite plays that captures this optimization problem, and with respect to this measure show the existence of an optimal winning strategy (if a winning strategy exists at all) and that it can be realized by a finite-state machine. For the latter claim we use a reduction to the solution of mean-payoff games due to Paterson and Zwick.

We consider infinite two-player games played on finite graphs where the winning condition (say for the first player) is given by a regular omega-language. We address issues of optimization in the construction of winning strategies in such games. Two criteria for optimization are discussed: memory size of finite automata that execute winning strategies, and - for games with liveness requests as winning conditions - ``waiting times'' for the satisfaction of requests. (For the first aspect we report on work of Holtmann and Löding, for the second on work of Horn, Wallmeier, and the author.)

Church's Problem, stated fifty years ago, asks for a finite-state machine that realizes the transformation of an infinite sequence alpha into an infinite sequence beta such that a requirement on (alpha, beta), expressed in monadic second-order logic, is satisfied. We explain how three fundamental techniques of automata theory play together in a solution of Church's Problem: Determinization (starting from the subset construction), appearance records (for stratifying acceptance conditions), and reachability analysis (for the solution of games).

Church's Problem (1957) asks for the construction of a finite-state procedure that transforms any input sequence alpha letter by letter into an output sequence beta such that the pair (alpha, beta) satisfies a given specification. Even after the solution by Büchi and Landweber in 1969 (for specifications in monadic second-order logic over the structure (N, +1)), the problem has stimulated research in automata theory for decades, in recent years mainly in the algorithmic study of infinite games. We present a modern solution which proceeds in several stages (each of them of moderate difficulty) and provides additional insight into the structure of the synthesized finite-state transducers.

We survey two basic techniques for showing that the monadic second-order theory of a structure is decidable. In the first approach, one deals with finite fragments of the theory (given for example by the restriction to formulas of a certain quantifier rank) and - depending on the fragment - reduces the model under consideration to a simpler one. In the second approach, one applies a global transformation of models while preserving decidability of the theory. We suggest a combination of these two methods.

Church's Problem (1962) asks for the construction of a procedure which, given a logical specification phi on sequence pairs, realizes for any input sequence X an output sequence Y such that (X,Y) satisfies phi. Büchi and Landweber (1969) gave a solution for MSO specifications in terms of finite-state automata. We address the problem in a more general logical setting where not only the specification but also the solution is presented in a logical system. Extending the result of Büchi and Landweber, we present several logics L such that Church's Problem with respect to L has also a solution in L, and we discuss some perspectives of this approach.

A model of dynamic networks is introduced which incorporates three kinds of network changes: deletion of nodes (by faults or sabotage), restoration of nodes (by actions of ``repair''), and creation of nodes (by actions that extend the network). The antagonism between the operations of deletion and restoration resp. creation is modelled by a game between the two agents ``Destructor'' and ``Constructor''. In this framework of dynamic model-checking, we consider as specifications (``winning conditions'' for Constructor) elementary requirements on connectivity of those networks which are reachable from some initial given network. We show some basic results on the (un-)decidability and hardness of dynamic model-checking problems.

Formal verification using the model checking paradigm has to deal with two aspects: The system models are structured, often as products of components, and the specification logic has to be expressive enough to allow the formalization of reachability properties. The present paper is a study on what can be achieved for infinite transition systems under these premises. As models we consider products of infinite transition systems with different synchronization constraints. We introduce finitely synchronized transition systems, i.e. product systems which contain only finitely many (parameterized) synchronized transitions, and show that the decidability of FO(R), first-order logic extended by reachability predicates, of the product system can be reduced to the decidability of FO(R) of the components. This result is optimal in the following sense: (1) If we allow semifinite synchronization, i.e. just in one component infinitely many transitions are synchronized, the FO(R)-theory of the product system is in general undecidable. (2) We cannot extend the expressive power of the logic under consideration. Already a weak extension of firstorder logic with transitive closure, where we restrict the transitive closure operators to arity one and nesting depth two, is undecidable for an asynchronous (and hence finitely synchronized) product, namely for the infinite grid.

Some classes of sets of vectors of natural numbers are introduced as generalizations of the semi-linear sets, among them the 'simple semi-polynomial sets.' Motivated by verification problems that involve arithmetical constraints, we show results on the intersection of such generalized sets with semi-linear sets, singling out cases where the non-emptiness of intersection is decidable. Starting from these initial results, we list some problems on solvability of arithmetical constraints beyond the semi-linear ones.

Expansions of the natural number ordering by unary predicates are studied, using logics which in expressive power are located between first-order and monadic second-order logic. Building on the model-theoretic composition method of Shelah, we give two characterizations of the decidable theories of this form, in terms of effectiveness conditions on two types of 201chomogeneous sets201d. We discuss the significance of these characterizations, show that the first-order theory of successor with extra predicates is not covered by this approach, and indicate how analogous results are obtained in the semigroup theoretic and the automata theoretic framework. This paper was written during a visit of the first author in Aachen in March 2006, funded by the European Science Foundation ESF in the Research Networking Programme AutoMathA (Automata: From Mathematics to Applications).

The two determinization procedures of Safra and Muller-Schupp for Büchi automata are compared, based on an implementation in a program called OmegaDet.

These lecture notes report on the use of automata theory in the study of infinite transition systems. This application of automata is an impor- tant ingredient of the current development of ``infinite-state system ver- ification'', and it provides an introduction into the field of ``algorithmic model theory'', a study of infinite models with an emphasis on computabil- ity results.

We investigate bottom-up and top-down deterministic automata on unranked trees. We show that for an appropriate definition of bottom-up deterministic automata it is possible to minimize the number of states efficiently and to obtain a unique canonical representative of the accepted tree language. For top-down deterministic automata it is well known that they are less expressive than the non-deterministic ones. By generalizing a corresponding proof from the theory of ranked tree automata we show that it is decidable whether a given regular language of unranked trees can be recognized by a top-down deterministic automaton. The standard deterministic top-down model is slightly weaker than the model we use, where at each node the automaton can scan the sequence of the labels of its successors before deciding its next move.

The two determinization procedures of Safra and Muller-Schupp for Büchi automata are compared, based on an implementation in a program called OmegaDet.

We report on recent progress in the study of infinite transition systems for which interesting properties (like reachability of designated states) can be checked algorithmically. Two methods for the generation of such models are discussed: the construction from simpler models via operations like unfolding and synchronized product, and the internal representation of state spaces by regular sets of words or trees.

In this paper we study, in the framework of mathematical logic, the class MetaReg of metaregular languages, i.e. the class of languages accepted by finite Time-Variant Automata (TVA) in the sense of Agasandyan [1] and Salomaa [6]. We set up a correspondence (in the style of Büchi-Elgot-Trakhtenbrot's Theorem for regular languages) between MetaReg and MSO[M], i.e. the class of languages definable in Monadic Second Order logic extended by fixed monadic numerical predicates. The number of monadic numerical predicates are used in the language yields an infinite hierarchy inside MSO[M].

Formal verification using the model-checking paradigm has to deal with two aspects. The systems models are structured, often as products of components, and the specification logic has to be expressive enough to allow the formalization of reachability properties. The present paper is a study on what can be achieved for infinite transition systems under these premises. As models we consider products of infinite transition systems with different synchronization constraints. We introduce finitely synchronized transition systems, i.e. product systems which contain only finitely many synchronized transitions, and show that the decidability of FO(R), first-order logic extended by reachability predicates, of the product system can be reduced to the decidability of FO(R) of the components in a Feferman-Vaught like style. This result is optimal in the following sense. (1) If we allow semifinite synchronization, i.e. just in one component infinitely many transitions are synchronized, the FO(R)-theory of the product system is in general undecidable. (2) We cannot extend the expressive power of the logic under consideration. Already a weak extension of first-order logic with transitive closure, where we restrict the transitive closure operators to arity one and nesting depth two, is undecidable for an asynchronous (and hence finitely synchronized) product, namely for the infinite grid.

Languages of infinite two-dimensional words (infinite omega-pictures) are studied in the automata theoretic setting of tiling systems. We show that a hierarchy of acceptance conditions as known from the theory of omega-languages can be established also over pictures. Since the usual pumping arguments fail, new proof techniques are necessary. Finally, we show that (unlike the case of omega-languages) none of the considered acceptance conditions leads to a class of infinitary picture languages which is closed under complementation.

We report on the development of e-lectures in theoretical computer science (more specifically, automata theory). The emphasis is on the development of a simple and flexible infrastructure, which reduces the effort in preparing e-lectures and tutorial units in this field of study. Two components are essential: an integrated and context-independent hardware and software system for the preparation and presentation of the course material, and a tutorial component with dialogue features, which allows to set up problems accompanying the lectures.

Es wird ein e-Lecture-System für die Theoretische Informatik vorgestellt, das seit drei Semestern an der RWTH Aachen für Vorlesungen der Automatentheorie erfolgreich eingesetzt wird. Grundlegende Zielsetzung war, eine einfach zu bedienende und flexible Infrastruktur zu schaffen. Im Zentrum stand dabei eine integrierte und flexibel einsetzbare Technik zur Vorbereitung und Präsentation des Kursmaterials, die sich durch sparsamen Einsatz von personellen und technischen Ressourcen auszeichnet. Wir stellen dieses System vor und diskutieren Erfahrungen und Perspektiven.

We present a method to solve certain infinite games over finite state spaces and apply this for the automatic synthesis of finite-state controllers. A lift-controller problem serves as an example for which the implementation of our algorithm has been tested. The specifications consist of safety conditions and so-called ``request-response-conditions'' (which have the form ``after visiting a state of P later a state of R is visited''). Many real-life problems can be modeled in this framework. We sketch the theoretical solution which synthesizes a finite-state controller for satisfiable specifications. The core of the implementation is a convenient input language (based on enriched Boolean logic) and a realization of the abstract algorithms with OBDD's (ordered binary decision diagrams).

We study infinite two-player games over pushdown graphs with a winning condition that refers explicitly to the infinity of the game graph: A play is won by player 0 if some vertex is visited infinity often during the play. We show that the set of winning plays is a proper Sigma_3-set in the Borel hierarchy, thus transcending the Boolean closure of Sigma_2-sets which arises with the standard automata theoretic winning conditions (such as the Muller, Rabin, or parity condition). We also show that this Sigma_3-game over pushdown graphs can be solved effectively (by a computation of the winning region of player 0 and his memoryless winning strategy). This seems to be a first example of an effectively solvable game beyond the second level of the Borel hierarchy.

The purpose of this tutorial is to survey the essentials of the algorithmic theory of infinite games, its role in automatic program synthesis and verification, and some challenges of current research.

We give a uniform treatment of the logical properties of alternating weak automata on infinite strings, extending and refining work of Muller, Saoudi, and Schupp (1984) and Kupferman and Vardi (1997). Two ideas are essential in the present set-up: There is no acyclicity requirement on the transition structure of weak alternating automata, and acceptance is defined only in terms of reachability of states; moreover, the run trees of the standard framework are replaced by run dags of bounded width. As applications, one obtains a new normal form for monadic second order logic, a simple complementation proof for weak alternating automata, and elegant connections to temporal logic.