Mitarbeiter

• Wolfgang Thomas
• Jan-Henrik Altenbernd
• Ingo Felscher
• Michael Holtmann
• Wong Karianto
• Christof Löding
• Daniel Neider
• Frank Radmacher
• Michaela Slaats
• Alex Spelten

Frühere Mitarbeiter

• Thierry Cachat
• Arnaud Carayol
• Mikhail Kats
• Oliver Matz
• Philipp Rohde
• Jens Vöge
• Nico Wallmeier
• Thomas Wilke
• Stefan Wöhrle

Motivated by problems in infinite-state verification, we study word rewriting systems that extend mixed prefix/suffix rewriting (short: bifix rewriting). We introduce several types of infix rewriting where infix replacements are subject to the condition that they have to occur next to tag symbols within a given word. Bifix rewriting is covered by the case where tags occur only as end markers. We show results on the reachability relation (or: derivation relation) of such systems depending on the possibility of removing or adding tags. Where possible we strengthen decidability of the derivation relation to the condition that regularity of sets is preserved, resp. that the derivation relation is even rational. Finally, we compare our model to ground tree rewriting systems and exhibit some differences.

The compositional method, introduced by Feferman and Vaught in 1959, allows to reduce the model-checking problem for a product structure to the model-checking problem for its factors. It applies to first-order logic, and limitations for its use have recently been revealed by Rabinovich (2007). We sharpen the results of Rabinovich by showing that the composition method is applicable to the asynchronous product (and the finitely synchronized product) for an extended modal logic in which the reachability modality is enhanced by a (semi-linear) condition on path lengths. We show that a slight extension leads to the failure of the composition theorem. We add comments on extensions of the result and open questions.

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 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.

Given a Rabin tree-language and natural numbers i,j, the language is said to be i,j-feasible if it is accepted by a parity automaton using priorities {i,i+1,...,j}. The i,j-feasibility induces a hierarchy over the Rabin-tree languages called the Mostowski hierarchy. In this paper we prove that the problem of deciding if a language is i,j-feasible is reducible to the uniform universality problem for distance-parity automata. Distance-parity automata form a new model of automata extending both the nested distance desert automata introduced by Kirsten in his proof of decidability of the star-height problem, and parity automata over infinite trees. Distance-parity automata, instead of accepting a language, attach to each tree a cost in omega+1. The uniform universality problem consists in determining if this cost function is bounded by a finite value.

In this paper we lift the result of Hashiguchi of decidability of the restricted star-height problem for words to the level of finite trees. Formally, we show that it is decidable, given a regular tree language L and a natural number k whether L can be described by a disjunctive mu-calculus formula with at most k nesting of fixpoints. We show the same result for disjunctive mu-formulas allowing substitution. The latter result is equivalent to deciding if the language is definable by a regular expression with nesting depth at most k of Kleene-stars. The proof, following the approach of Kirsten in the word case, goes by reduction to the decidability of the limitedness problem for non-deterministic nested distance desert automata over trees. We solve this problem in the more general framework of alternating tree automata.

We investigate rational relations over trees. Our starting point is the definition of rational tree relations via rational expressions by Raoult (Bull.Belg.Math.Soc. 1997). We develop a new class of automata, called asynchronous tree automata, which recognize exactly these relations. The automata theoretic approach is convenient for the solution of algorithmic problems (like the emptiness problem). The second contribution of this paper is a new subclass of the rational tree relations, called separate-rational tree relations, defined via a natural restriction on asynchronous tree automata. These relations are closed under composition, preserve regular tree languages, and generate precisely the regular sets in the unary case (all these properties fail for the general model), and they are still more powerful than, for instance, the automatic tree relations.

We investigate rational relations over trees. Our starting point is the definition of rational tree relations via rational expressions by Raoult (Bull.Belg.Math.Soc. 1997). We develop a new class of automata, called asynchronous tree automata, which recognize exactly these relations. The automata theoretic approach is convenient for the solution of algorithmic problems (like the emptiness problem). The second contribution of this paper is a new subclass of the rational tree relations, called separate-rational tree relations, defined via a natural restriction on asynchronous tree automata. These relations are closed under composition, preserve regular tree languages, and generate precisely the regular sets in the unary case (all these properties fail for the general model), and they are still more powerful than, for instance, the automatic tree relations.

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.

Kurzfassung in Deutsch: Gegenstand dieser Arbeit sind Lösungsverfahren für unendliche Spiele und die Implementierung entsprechender Algorithmen im Rahmen einer Experimentierplattform. Der Schwerpunkt liegt auf Spielen mit Gewinnbedingungen, welche gewisse Liveness-Eigenschaften fordern. Eine für Anwendungen (etwa in der Controller-Synthese) zentrale Liveness-Eigenschaft ist die `Request-Response-Bedingung'. Sie ist eine Konjunktion von Bedingungen der folgenden Gestalt: Immer wenn ein `Request'-Zustand besucht wird, folgt irgendwann später auch der Besuch eines entsprechenden `Response'-Zustandes. Eng verwandt damit sind die sogenannten `Streett-Bedingungen', in denen für wiederholte Besuche gewisser Zustände wiederholte Besuche anderer Zustände gefordert werden. Es werden verschiedene Lösungsverfahren für Request-Response-Spiele und Streett-Spiele vorgestellt, mit Anwendungen etwa in der Analyse von Live-Sequence-Charts. Der Hauptbeitrag besteht in einer quantitativen Analyse der Request-Response-Spiele. Ein natürlicher Ansatz zur quantitativen Abstufung von Gewinnstrategien berücksichtigt die Wartezeiten, die in einer unendlichen Partie zwischen den Besuchen von `Request'- und nachfolgenden `Response'-Zuständen verstreichen. Dazu werden verschiedene Qualitätsmase für Partien in Request-Response-Spielen (über endlichen Spielgraphen) eingeführt und diskutiert. Für Mase, in denen die `Strafe' mehr als linear in den Wartezeiten steigt, wird eine algorithmische Berechnung optimaler Gewinnstrategien vorgestellt. Kernpunkt ist eine Reduktion auf Mean-Payoff-Spiele über endlichen Zustandsräumen, mit der zugleich gezeigt wird, dass optimale Strategien durch endliche Automaten implementierbar sind. Die Experimentierplattform GaSt (`Games, Automata \& Strategies') integriert zahlreiche Algorithmen zur Theorie der Omega-Automaten und zur Lösung unendlicher Spiele.

Abstract in english: In this thesis we develop methods for the solution of infinite games and present implementations of corresponding algorithms in the framework of a platform for the experimental study of automata theoretic algorithms. Our focus is on games with winning conditions that express certain liveness properties. A central type of liveness requirement in applications (e.g., in controller synthesis) is the ``request-response condition''. It has the form of a conjunction of conditions ``Whenever a `request'-state is visited, sometime later a corresponding `response'-state is visited''. A closely related winning condition is the ``Streett condition'' in which for repeated visits of certain states the repeated visits of other states is required. We present methods for the solution of request-response games and Streett games, the latter with an application in the analysis of live-sequence-charts. The main contribution is a quantitative analysis of request-response games. We pursue a natural approach for the quantitative evaluation of winning strategies by taking into account the waiting times that elapse between visits of ``request''-states and subsequent visits of ``response''-states in an infinite play. We introduce and discuss several related measures of plays in request-response games (over finite game arenas). For measures that induce a ``penalty'' which grows more than linearly in the waiting times, we present an algorithm to compute optimal winning strategies. The core of the argument is a reduction to mean-payoff games over finite arenas; it also shows that optimal strategies are implementable by finite-state machines. The experimental platform GaSt (``Games, Automata & Strategies'') offers numerous algorithms of the theory of omega-automata and for the solution of infinite games.

We give a new proof showing that it is not possible to define in monadic second-order logic (MSO) a choice function on the infinite binary tree. This result was first obtained by Gurevich and Shelah using set theoretical arguments. Our proof is much simpler and only uses basic tools from automata theory. We discuss some applications of the result concerning unambiguous tree automata and definability of winning strategies in infinite games. In a second part we strengthen the result of the non-existence of an MSO-definable well-founded order on the infinite binary tree by showing that every infinite binary tree with a well-founded order has an undecidable MSO-theory.

We consider a new kind of interpretation over relational structures: finite sets interpretations. Those interpretations are defined by weak monadic second-order (WMSO) formulas with free set variables. They transform a given structure into a structure with a domain consisting of finite sets of elements of the orignal structure. The definition of these interpretations directly implies that they send structures with a decidable WMSO theory to structures with a decidable first-order theory. In this paper, we investigate the expressive power of such interpretations applied to infinite deterministic trees. The results can be used in the study of automatic and tree-automatic structures.

In this thesis we deal with the problem of reducing the memory necessary for implementing winning strategies in infinite games. We present an algorithm that is based on the notion of game reduction. There, the idea is to reduce the problem of computing a solution to a given game to computing a solution to a new game. This new game has an extended game graph which contains the memory to solve the original game. Our algorithm computes an equivalence relation on the vertices of the extended game graph and from that deduces equivalent memory contents. The computations are carried out via a transformation to omega-automata. We apply our algorithm to Request-Response and Staiger-Wagner games where in both cases we obtain a running time exponential in the size of the given game graph. We compare our method to another technique of memory reduction, namely the minimisation algorithm for finite automata with output. For each of the two approaches we present an example for which it yields a substantially better result than the other approach.

We deal with the problem of reducing the memory necessary for implementing winning strategies in infinite games. We present an algorithm that is based on the notion of game reduction. The key idea of a game reduction is to reduce the problem of computing a solution for a given game to the problem of computing a solution for a new game which has an extended game graph but a simpler winning condition. The new game graph contains the memory to solve the original game. Our algorithm computes an equivalence relation on the vertices of the extended game graph and from that deduces equivalent memory contents. We apply our algorithm to Request-Response and Staiger-Wagner games where in both cases we obtain a running time polynomial in the size of the extended game graph. We compare our method to the technique of minimising strategy automata and present an example for which our approach yields a substantially better result.

We propose an extension of the tree automata with constraints between direct subtrees (Bogaert and Tison, 1992) to unranked trees. Our approach uses MSO-formulas to capture the possibility of comparing unboundedly many direct subtrees. Our main result is that the nonemptiness problem for the deterministic automata, as in the ranked setting, is decidable. Furthermore, we show that the nondeterministic automata are more expressive than the deterministic ones.

We extend the propositional dynamic logic PDL of Fischer and Ladner with a restricted kind of recursive programs using the formalism of visibly pushdown automata (Alur, Madhusudan 2004). We show that the satisfiability problem for this extension remains decidable, generalising known decidability results for extensions of PDL by non-regular programs. Our decision procedure establishes a 2-ExpTime upper complexity bound, and we prove a matching lower bound that applies already to rather weak extensions of PDL with non-regular programs. Thus, we also show that such extensions tend to be more complex than standard PDL.

We investigate algorithmic properties of infinite transition graphs that are generated by rewriting systems over unranked trees. Two kinds of such rewriting systems are studied. For the first, we construct a reduction to ranked trees via an encoding and to standard ground tree rewriting, thus showing that the generated classes of transition graphs coincide. In the second rewriting formalism, we use subtree rewriting combined with a new operation called flat prefix rewriting and show that strictly more transition graphs are obtained while the first-order theory with reachability relation remains decidable.

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.

Abstract: Automata definable relations over words are widely investigated. In the case of words recognizable, automatic, deterministic rational, and (nondeterministic) rational relations result in a well-known hierarchy. We adapt these classes of relations to trees in a natural manner so that the familiar properties of word relations are preserved for the most part. In the main part of this thesis we deal with rational relations over trees. On the one hand we consider rational tree relations introduced by Raoult (Bull.Belg.Math.Soc. 1997), on the other hand we define so-called separate-rational tree relations which form a subclass of rational tree relations. Rational relations over words and trees can be defined inductively by their closure properties. In this thesis we also develop classes of automata, namely asynchronous tree automata and separate-asynchronous tree automata, which recognize exactly the classes of rational and separate-rational tree relations. The classes of automata enable the definition of deterministic relations over trees yielding a whole hierarchy of tree relations. Automata definable relations also enable the definition of relations over unranked trees. We gather differences to the ranked cases and discuss in what way these classes coincide by considering binary encodings of unranked trees.

Zusammenfassung: Automatendefinierbare Relationen über Wörtern sind weitgehend erforscht. Im Fall von Wörtern bilden erkennbare, automatische, deterministisch rationale und (nichtdeterministisch) rationale Relationen eine wohlbekannte Hierarchie. Wir übertragen diese Klassen von Relationen auf natürliche Weise auf Bäume, so dass die von Wortrelationen vertrauten Eigenschaften gröstenteils erhalten bleiben. Im Hauptteil dieser Arbeit beschäftigen wir uns mit rationalen Relationen über Bäumen. Zum einen betrachten wir die von Raoult eingeführten rationalen Baumrelationen (Bull.Belg.Math.Soc. 1997), zum anderen definieren wir sogenannte separiert-rationale Baumrelationen, die eine Unterklasse der rationalen Baumrelationen bilden. Rationale Relationen über Wörtern und Bäumen lassen sich induktiv über ihre Abschlusseigenschaften definieren. In dieser Arbeit entwickeln wir aber auch Automatenmodelle, und zwar asynchrone Baumautomaten und separiert-asynchrone Baumautomaten, welche gerade die Klassen der rationalen und der separiert-rationalen Baumrelationen erkennen. Die Automatenmodelle ermöglichen die Definition von deterministischen Relationen über Bäumen, welche zu einer ganzen Hierarchie von Baumrelationen führen. Automatendefinierbare Relationen ermöglichen auch die Definition von Relationen über unbeschränkt verzweigten Bäumen. Wir erarbeiten Unterschiede zu den beschränkt verzweigten Fällen und diskutieren, inwiefern diese Klassen bei der Betrachtung binärer Kodierungen von unbeschränkt verzweigten Bäumen übereinstimmen.

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.

In this thesis we deal with games over infinite graphs with regular winning conditions. A well studied family of such games are the pushdown games. An important result for these games is that the winning region can be described by regular sets of configurations. We extend this result to games defined by higher-order pushdown systems. The higher-order pushdown systems extend the usual pushdown systems by the use of higher-order stacks which are stacks of stacks of stacks etc.. We concentrate in this thesis just on level 2 stacks that are stacks that contain a sequence of level 1 stacks but the results can easily be lifted to level n. The operations to manipulate those stacks are the simple level 1 operations push and pop and also operations that can copy and destroy the topmost level 1 stacks inside the level 2 stack. For the definition of regularity over higher-order pushdown stacks we use a technique recently developed by Carayol in 2005. We will present an algorithm to compute the winning regions of reachability and parity games over higher-order pushdown graphs.

Visibly pushdown automata are special pushdown automata whose stack behavior is driven by the input symbols according to a partition of the alphabet. We show that it is decidable for a given visibly pushdown automaton whether it is equivalent to a visibly counter automaton, i.e. an automaton that uses its stack only as counter. In particular, this allows to decide whether a given visibly pushdown language is a regular restriction of the set of well-matched words, meaning that the language can be accepted by a finite automaton if only well-matched words are considered as input.

Planar spatial datasets can be modeled by closed semi-algebraic sets in the plane. We establish a characterization of the topological properties of such datasets expressible in the relational calculus with real polynomial constraints. The characterization is in the form of a query language that can only point that can only talk about points in the set and the 'cones' around these points.

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.

We propose an extension of the tree automata with constraints between direct subtrees (Bogaert and Tison, 1992) to unranked trees. Our approach uses MSO-formulas to capture the possibility of comparing unboundedly many direct subtrees. Our main result is that the nonemptiness problem for the deterministic automata, as in the ranked setting, is decidable. It turns out that the main difficulty is indeed the absence of the rank, as it gives a certain bound on the number of distinct subtrees needed in order to satisfy an equality or disequality constraint. We overcome this difficulty by finding such a bound via a brute-force method.

We consider the transition graphs of regular ground tree (or term) rewriting systems. The vertex set of such a graph is a (possibly infinite) set of trees. Thus, with a finite tree automaton one can represent a regular set of vertices. It is known that the backward closure of sets of vertices under the rewriting relation preserves regularity, i.e., for a regular set T of vertices the set of vertices from which one can reach T can be accepted by a tree automaton. The main contribution of this paper is to lift this result to the recurrence problem, i.e., we show that the set of vertices from which one can reach infinitely often a regular set T is regular, too. Since this result is effective, it implies that the problem whether, given a tree t and a regular set T, there is a path starting in t that infinitely often reaches T, is decidable. Furthermore, it is shown that the problems whether all paths starting in t eventually (respectively, infinitely often) reach T, are undecidable. Based on the decidability result we define a fragment of temporal logic with a decidable model-checking problem for the class of regular ground tree rewriting graphs.

We extend the propositional dynamic logic PDL of Fischer and Ladner with a restricted kind of recursive programs using the formalism of visibly pushdown automata (Alur, Madhusudan 2004). We show that the satisfiability problem for this extension remains decidable, generalising known decidability results for extensions of PDL by non-regular programs.

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).

We study logics and games over dynamically changing structures. Van Benthem?s sabotage modal logic consists of modal logic with a cross-model modality referring to submodels from which a transition has been removed. We add constructors for forming least and greatest monadic fixed-points to that logic and obtain the sabotage ?-calculus. We introduce backup parity games as an extension of standard parity games where in addition, both players are able to delete edges of the arena and to store, resp., restore the current appearance of the arena by use of a fixed number of registers. We show that these games serve as model checking games for the sabotage ?-calculus, even if the access to registers follows a stack discipline. The problem of solving the games with restricted register access turns out to be PSPACE-complete while the more general games without a limited access become EXPTIME-complete (for at least three registers).

In the classical framework of graph algorithms, program logics, and corresponding model checking games, one considers changes of system states and movements of agents within a system, but the underlying graph or structure is assumed to be static. This limitation motivates a more general approach where dynamic changes of structures are relevant. In this thesis, we take up a proposal of van Benthem from 2002 and consider games and modal logics over dynamically changing structures, where we focus on the deletion of edges of a graph, resp., transitions of a Kripke structure. We investigate two-player games where one player tries to reach a designated vertex of a graph while the opponent sabotages this by deleting edges. It is shown that adding the `saboteur' makes these games algorithmically much harder to solve. Further, we analyze corresponding modal logics which are augmented with cross-model modalities referring to submodels from which a transition has been removed. On the one hand, it turns out that these `sabotage modalities' already strengthen standard modal logic in such a way that many nice algorithmic and model-theoretic properties get lost. On the other hand, the model checking problem remains decidable. The main limitation of modal logic is the lack of a mechanism for unbounded iteration or recursion. To overcome this, we augment the `sabotage modal logics' of the first part of the thesis with constructors for forming least and greatest monadic fixed-points. The resulting logic extends the well-known ?-calculus and is capable of expressing iterative properties like reachability or recurrence as well as basic changes of the underlying Kripke structure, namely, the deletion of transitions. Finally, we introduce extended parity games where in addition, both players are able to delete edges of the arena and to store, resp., restore the current appearance of the arena by use of a fixed number of registers. We show that these games serve as model checking games for the aforementioned `sabotage mu-calculus'.

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

Finite graphs constitute an important tool in various fields of computer science. In order to transfer the theory of finite graphs at least partially to infinite systems, a finite representation of infinite systems is needed. Rewriting systems form a practical model for the finite representation of infinite graphs. Among attractive subclasses of rewriting systems is the class of ground tree rewriting systems over ranked trees, which is known to have good algorithmic properties. We investigate these algorithmic properties for two kinds of rewriting systems over unranked trees. For the first introduced rewriting formalism, we define a reduction to ranked (binary) trees via an encoding and also to standard ground tree rewriting, and we show that the generated classes of transition graphs coincide. For the second introduced rewriting formalism over unranked trees using subtree rewriting combined with flat prefix rewriting, we obtain strictly more transition graphs, and we show that the reachability problem over such graphs is still decidable. Here, a flat prefix rewrite rule substitutes a prefix of the word derived from the front of a subtree of height 1. However, as opposed to standard ground tree rewriting systems, this decidability result fails for both formalisms when the transition graphs are restricted by a deterministic top down tree automaton.

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.

We analyze models of infinite-state automata extended by monotonic counting mechanisms, starting from the (finite-state) Parikh automata studied by Klaedtke and Rueß. We show that, for linear-bounded automata, this extension does not increase the language recognition power. In the framework of infinite transition systems developed by Caucal and others, we show that adding monotonic counters to synchronized rational graphs still results in synchronized rational graphs, in contrast to the case of pushdown graphs or prefix-recognizable graphs. For prefix-recognizable graphs, however, we show that the extension by monotonic counters retains the decidability of the reachability problem.

We introduce the notion of semi-polynomial sets, generalizing the notion of semi-linear sets, and show that each semi-polynomial set is the Parikh image of level 2 pushdown automata, which represent a special class of higher-order pushdown automata.

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.

The extension of formal verification methods to infinite models requires classes of graphs which are finitely representable and for which the model checking problem is decidable. We consider three approaches to define classes of finitely representable graphs: internal representations as configuration graphs of higher-order pushdown systems, transformational representations by application of operations which preserve the decidability of the model checking problem, and by composition from components using synchronized products.

Closed semi-algebraic sets in the plane form a powerful model of planar spatial datasets. We establish a characterization of the topological properties of such datasets expressible in the relational calculus with real polynomial constraints. The characterization is in the form of a query language that can only talk about points in the set and the ``cones'' around these points.

We propose here Live Sequence Charts with a new, game-based semantics to model interactions between the system and its environment. For constructing programs automatically, we give an algorithm to synthesize either a strategy for the system ensuring that the specification is respected, or, if the specification is unimplementable, a strategy for the environment forcing the system to fail. We introduce the concept of mercifulness, a desirable property of the synthesized program. We give a polynomial time algorithm for synthesizing merciful winning strategies.

We introduce top-down deterministic transducers with rational lookahead (transducer for short) working on infinite terms. We show that for such a transducer T', there exists an MSO-transduction T such that for any graph G, unfold(T(G))=T'(unfold(G)). Reciprocally, we show that if an MSO-transduction T ``preserves bisimilarity'', then there is a transducer T' such that for any graph G, unfold(T(G)) = T'(unfold(G)). According to this, transducers can be seen as a complete method of implementation of MSO-transductions that preserve bisimilarity. One application is for transformations of equational systems.

We prove an existential version of Gaifman's locality theorem and show how it can be applied algorithmically to evaluate existential first-order sentences in finite structures.

We investigate the possibilities of extending the idea underlying Parikh automata of Klaedtke and Rueß to pushdown automata (PDA) and level 2 pushdown automata (2PDA), which are automata augmented with stacks consisting of stacks. For the former, we show that the emptiness problem is still decidable and that the languages recognized are context-sensitive. For the latter, we investigate the Parikh images of 2PDA-recognizable languages. We extend the framework of semi-linear sets to the so-called semi-polynomial sets and show that 2PDA's can generate all these sets. However, we also show that there are 2PDA-recognizable languages whose Parikh images are not semi-polynomial. For the issue of using semi-polynomial sets as the constraint sets of Parikh automata, we investigate the emptiness problem for the intersection of a semi-linear set and a semi-polynomial set. We show two partial results: first, weakening the framework of semi-linear sets leads to decidability, and second, strengthening the framework of semi-polynomial sets leads to undecidability. Finally, we also consider the application of the idea underlying Parikh automata to infinite graphs.

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].

The class of visibly pushdown languages has been recently defined as a subclass of context-free languages with desirable closure properties and tractable decision problems. We study visibly pushdown games, which are games played on visibly pushdown systems where the winning condition is given by a visibly pushdown language. We establish that, unlike pushdown games with pushdown winning conditions, visibly pushdown games are decidable and are 2EXPTIME-complete. We also show that pushdown games against LTL specifications and CARET specifications are 3EXPTIME-complete. Finally, we establish the topological complexity of visibly pushdown languages by showing that they are a subclass of Boolean combinations of Sigma_3 sets. This leads to an alternative proof that visibly pushdown automata are not determinizable and also shows that visibly pushdown games are determined.

In this paper we continue the study of 'sabotage modal logic' SML which was suggested by van Benthem. In this logic one describes the progression along edges of a transition graph in alternation with moves of a saboteur who can delete edges. A drawback of the known results on SML is the asymmetry of the two modalities of 'moving' and 'deleting': Movements are local, whereas there is a global choice for edge deletion. To balance the situation and to obtain a more realistic model for traffic and network problems, we require that also the sabotage moves (edge deletions) are subject to a locality condition. We show that the new logic, called path sabotage logic PSL, already has the same complexities as SML (model checking, satisfiability) and that it lacks the finite model property. The main effort is finding a pruned form of SML-models that can be enforced within PSL and giving appropriate reductions from SML to PSL.

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.

Two player games are a standard model of reactive computation, where e.g. one player is the controller and the other is the environment. A game is won by a player if she has a winning strategy, i.e., if she can win every play. Given a finite description of the game, our aim is to compute the winner and a winning strategy. For finite graphs these problems have been solved for a long time, although some complexity questions remain open. We consider several classes of infinite graphs, from transition graphs of pushdown automata up to graphs of the Caucal hierarchy, and we investigate different winning conditions: reachability, recurrence (Büchi), parity, and a Sigma_3-condition. Two kinds of techniques are developed: a symbolic approach based on finite automata recognizing infinite sets of configurations and a game simulation which reduces a given game into a simpler one and solves it. Different kinds of strategies are also constructed: either positional or based on pushdown stack memories.

We consider two-player parity games played on transition graphs of higher order pushdown automata. They are ``game-equivalent'' to a kind of model-checking game played on graphs of the infinite hierarchy introduced recently by Caucal. Then in this hierarchy we show how to reduce a game to a graph of lower level. This leads to an effective solution and a construction of the winning strategies.

In this paper we give two equivalent characterizations of the Caucal hierarchy, a hierarchy of infinite graphs with a decidable monadic second-order (MSO) theory. It is obtained by iterating the graph transformations of unfolding and inverse rational mapping. The first characterization sticks to this hierarchical approach, replacing the language-theoretic operation of a rational mapping by an MSO-transduction and the unfolding by the treegraph operation. The second characterization is non-iterative. We show that the family of graphs of the Caucal hierarchy coincides with the family of graphs obtained as the epsilon-closure of configuration graphs of higher-order pushdown automata. While the different characterizations of the graph family show their robustness and thus also their importance, the characterization in terms of higher-order pushdown automata additionally yields that the graph hierarchy is indeed strict.

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.

We consider the sabotage game presented by van Benthem in an essay on the occasion of Jörg Siekmann's 60th birthday. In this game one player moves along the edges of a finite, directed or undirected multi-graph and the other player takes out a link after each step. There are several algorithmic tasks over graphs which can be considered as winning conditions for this game, for example reachability, Hamilton path or complete search. As the game definitely ends after at most the number of edges (counted with multiplicity) steps, it is easy to see that solving the sabotage game for the mentioned tasks takes at most PSPACE in the size of the graph. We will show that on the other hand solving this game in general is PSPACE-hard for all conditions. We extend this result to some variants of the game (removing more than one edge per round and removing vertices instead of edges). Finally we introduce a modal logic over changing models to express tasks corresponding to the sabotage games. We will show that model checking this logic is PSPACE-complete.

We consider the sabotage game as presented by van Benthem. In this game one player moves along the edges of a finite multi-graph and the other player takes out a link after each step. One can consider usual algorithmic tasks like reachability, Hamilton path, or complete search as winning conditions for this game. As the game definitely ends after at most the number of edges steps, it is easy to see that solving the sabotage game for the mentioned tasks takes at most PSPACE in the size of the graph. In this paper we establish the PSPACE-hardness of this problem. Furthermore, we introduce a modal logic over changing models to express tasks corresponding to the sabotage games and we show that model checking this logic is PSPACE-complete.

We consider the sabotage modal logic SML which was suggested by van Benthem. SML is the modal logic equipped with a ‘transition-deleting’ modality and hence a modal logic over changing models. It was shown that the problem of uniform model checking for this logic is PSPACE-complete. In this paper we show that, on the other hand, the formula complexity and the program complexity are linear, resp., polynomial time. Further we show that SML lacks nice model-theoretic properties such as bisimulation invariance, the tree model property, and the finite model property. Finally we show that the satisfiability problem for SML is undecidable. Therefore SML seems to be more related to FO than to usual modal logic.

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).

For any language L, let pow(L)={u^j | j>= 0, uin L} be the set of powers of elements of L. Given a rational language L (over a finite alphabet), we study the question, posed in [Cal 96], whether pow(L) is rational or not. While leaving open the problem in general, we provide an algorithmic solution for the case of one-letter alphabets. This case is still non trivial; our solution is based on Dirichlet's result that for two relatively prime numbers, their associated arithmetic progression contains infinitely many primes.

We consider infinite two-player games on pushdown graphs, the reachability game where the first player must reach a given set of vertices to win, and the Büchi game where he must reach this set infinitely often. We provide an automata theoretic approach to compute uniformly the winning region of a player and corresponding winning strategies, if the goal set is regular. Two kinds of strategies are computed: positional ones which however require linear execution time in each step, and strategies with pushdown memory where a step can be executed in constant time.

The transition graph of the pushdown automaton defines the arena: the graph of the play and the partition of the vertex set needed to specify the parity winning condition. We know that such games are determined and that each of both players has a memoryless winning strategy on his winning region. The aim of this paper is to show how to compute effectively the winning region of Player 0 and a memoryless winning strategy. The idea is to simulate the pushdown system in the full W-tree, where W is a finite set of directions, and to use the expressive power of alternating two-way tree automata to answer these questions. Finally it is necessary to translate the 2-way tree automaton into an equivalent nondeterministic one-way tree automaton.

Walukiewicz gave in 1996 a solution for parity games on pushdown graphs: he proved the existence of pushdown strategies and determined the winner with an EXPTIME procedure. We give a new presentation and a new algorithmic proof of these results, obtain a uniform solution for parity games (independent of their initial configuration), and extend the results to prefix-recognizable graphs. The winning regions of the players are proved to be effectively regular, and winning strategies are computed.

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.

We analyze structural properties of ground tree rewriting graphs, generated by rewriting systems that perform replacements at the front of finite, ranked trees. The main result is that the class of ground tree rewriting graphs of bounded tree width exactly corresponds to the class of pushdown graphs. Furthermore we show that ground tree rewriting graphs of bounded clique width also have bounded tree width.

We consider infinite graphs that are generated by ground tree (or term) rewriting systems. The vertices of these graphs are trees. Thus, with a finite tree automaton one can represent a regular set of vertices. It is shown that for a regular set T of vertices the set of vertices from where one can reach (respectively, infinitely often reach) the set T is again regular. Furthermore it is shown that the problems, given a tree t and a regular set T, whether all paths starting in t eventually (respectively, infinitely often) reach T, are undecidable. We then define a logic which is in some sense a maximal fragment of temporal logic with a decidable model-checking problem for the class of ground tree rewriting graphs.

This note combines an unpublished theorem of Woodin's about AD and Uniformisation with combinatorial arguments of Blass' to get a startling consequence for games on $\omega$ of length $\omega \times 2$: The determinacy of these games is equivalent to the Axiom of Real Determinacy.

We consider monadic second order logic (MSO) and the propositional $\mu$-calculus ($L$_μ) over transition systems. It is well known that every class of transition systems which is definable by a sentence of $L$_μ is definable by a sentence of MSO as well. It will be shown that the converse is also true for an important fragment of MSO: every class of transition systems which is MSO-definable and which is closed under bisimulation - i.e., the sentence does not distinguish between bisimilar models - is also $L$_μ-definable. Hence we obtain the following expressive completeness result: the bisimulation invariant fragment of MSO and $L$_μ are equivalent. The result was proved by David Janin and Igor Walukiewicz. Our presentation is based on their article [JW96]. The main step is the development of automata-based characterizations of $L$_μ over arbitrary transition systems and of MSO over transition trees. It turns out that there is a general notion of automaton subsuming both characterizations, so we obtain a common ground to compare these two logics. Further we need the notion of the $\omega$-unravelling for a transition system, on the one hand to obtain a bisimilar transition tree and on the other hand to increase the possibilities of choosing successors.

We start with a section introducing the notions of transition systems and transition trees, bisimulations and the $\omega$-unravelling. In Section 3 we repeat the definitions of MSO and $L$_μ. In Section 4 we develop a general notion of automaton and acceptance conditions in terms of games to obtain the characterizations of the two logics. In the last section we will prove the main result mentioned above.

[JW96] David Janin and Igor Walukiewicz, On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic, Proceedings of the 7th International Conference on Concurrency Theory, CONCUR'96 (U. Montanari and V. Sassone, eds.), Lecture Notes in Computer Science, vol. 1119, Springer-Verlag, August 1996, pp. 263-277.

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.

For any language L, let pow(L)={u^j | j >= 0, uin L} be the set of powers of elements of L. Given a rational language L (over a finite alphabet), we study the question, posed in [Cal 96], whether pow(L) is rational or not. While leaving open the problem in general, we provide an algorithmic solution for the case of one-letter alphabets. This case is still non trivial; our solution is based on Dirichlet's result that for two relatively prime numbers, their associated arithmetic progression contains infinitely many primes.

Gaifman's locality theorem (1981) states that every first-order sentence is equivalent to a Boolean combination of sentences saying: There exist elements a₁,...,a_k that are far apart from one another, and each a_i satisfies some local condition described by a first-order formula. We prove that every existential first-order sentence is equivalent to a positive Boolean combination of sentences saying: There exist elements a₁,...,a_k that are far apart from one another, and each a_i satisfies some local condition described by an existential first-order formula. We then show how a variant of this existential locality theorem can be applied to evaluate existential first-order sentences in certain finite structures, such as planar graphs or graphs of bounded degree, improving a result of Frick and Grohe (1999) for the special case of existential sentences.

We analyze the minimization problem for deterministic weak automata, a subclass of deterministic Büchi automata, which recognize the regular languages that are recognizable by deterministic Büchi and deterministic co-Büchi automata. We reduce the problem to the minimization of finite automata on finite words and obtain an algorithm running in time O(n log(n)), where n is the number of states of the automaton.

We are considering infinite two-person games with perfect information. The Axiom of Determinacy AD is the following statement: every game of length $\omega$, where both players choose integers is determined, i.e., one of the two players has a winning strategy. In Chapter 2 we give a short review of the mathematical formalism of the considered games and the notion of determinacy and we discuss some elementary consequences of the Axiom of Determinacy.

We are investigating extensions of this axiom. First of all there are two parameters which can be changed to obtain new games: the complexity of the particular moves (in the AD context: natural numbers) and the length of the game, measured by the transfinite scale of the ordinals (in the AD context: omega). In Chapter 3 we discuss the appropriate determinacy hypotheses, in particular their boundaries and the dependencies among each other. For example we show the Theorem of Blass, which says that the determinacy of all games on reals with length $\omega$ is equivalent to that of all games on integers with length $\omega 2$.

The main result is a classification of all determinacy hypotheses for games on integers of a fixed countable length. All these hypotheses are equivalent either to AD or to the stronger Axiom of Real Determinacy AD_R. The exact boundary in regard to the length of the games is $\omega *2$. This statement combines an unpublished theorem of Woodin about AD and Uniformisation with the mentioned theorem of Blass.

In Chapter 4 we consider the relative consistency strength of determinacy hypotheses. We show the existence of constructible models of determinacy and discuss some aspects of the correlation with the theory of large cardinals. It can be shown that under the assumption of determinacy in the universe the canonical constructible model L(R) is indeed a model of AD. But L(R) cannot be a model of the stronger axiom AD_R.

AD⁺ is an axiom introduced by Woodin to combine consequences of AD_R with the relative consistency with V=L(R). In Chapter 5, we introduce AD⁺ and show its relative consistency with V=L(R). These results are due to Woodin (unpublished). It is still open whether AD⁺ is a proper extension of AD.

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.

In this paper we settle the complexity of some basic constructions of omega-automata theory, concerning transformations of automata characterizing the set of omega-regular languages. In particular we consider Safra's construction (for the conversion of nondeterministic Büchi automata into deterministic Rabin automata) and the appearance record constructions (for the transformation between different models of deterministic automata with various acceptance conditions). Extending results of Michel (1988) and Dziembowski, Jurdzinski, and Walukiewicz (1997), we obtain sharp lower bounds on the size of the constructed automata.