Publikationen

Nach Autoren

Mitarbeiter

Frühere Mitarbeiter

Nach Erscheinungsjahr

To appear

[CG14a] Namit Chaturvedi and Marcus Gelderie. Classifying regular infinitary trace langauges using word automata. In MFCS 2014: 39th International Symposium on Mathematical Foundations of Computer Science, Lecture Notes in Computer Science, 2014. To appear.

We address the problem of providing a Borel-like classification of languages of infinite Mazurkiewicz traces, and provide a solution in the framework of omega-automata over infinite words - which is invoked via the sets of linearizations of infinitary trace languages. We identify trace languages whose linearizations are recognized by deterministic weak or deterministic Buechi (word) automata. We present a characterization of the class of linearizations of all omega-regular trace languages in terms of Muller (word) automata. Finally, we show that the linearization of any omega-regular trace language can be expressed as a Boolean combination of languages recognized by our class of deterministic Buechi automata.

[CKLV13] T. Colcombet, D. Kuperberg, C. Löding, and M. Vanden Boom. Deciding the weak definability of Büchi definable tree languages. In Proceedings of the 22nd Annual Conference of the European Association for Computer Science Logic, CSL 2013, Leibniz International Proceedings in Informatics (LIPIcs). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013. to appear. (c) Springer.
[ pdf ]

Weakly definable languages of infinite trees are an expressive subclass of regular tree languages definable in terms of weak monadic second-order logic, or equivalently weak alternating automata. Our main result is that given a Büchi automaton, it is decidable whether the language is weakly definable. We also show that given a parity automaton, it is decidable whether the language is recognizable by a nondeterministic co-Büchi automaton. The decidability proofs build on recent results about cost automata over infinite trees. These automata use counters to define functions from infinite trees to the natural numbers extended with infinity. We reduce to testing whether the functions defined by certain ``quasi-weak'' cost automata are bounded by a finite value.

2014

[Cha14b] Namit Chaturvedi. Toward a structure theory of regular infinitary trace languages. In ICALP 2014: 41st International Colloquium on Automata, Languages, and Programming, Part II, number 8573 in Lecture Notes in Computer Science, pages 134-145, 2014.
[ pdf ]

The family of regular languages of infinite words is structured into a hierarchy where each level is characterized by a class of deterministic omega-automata - the class of deterministic Büchi automata being the most prominent among them. In this paper, we analyze the situation of regular languages of infinite Mazurkiewicz traces that model non-terminating, concurrent behaviors of distributed systems. Here, a corresponding classification is still missing. We introduce the model of ``synchronization-aware asynchronous automata'', which allows us to initiate a classification of regular infinitary trace languages in a form that is in nice correspondence to the case of omega-regular word languages.

[Cha14a] Namit Chaturvedi. Languages of infinite traces and deterministic asynchronous automata. Technical Report AIB-2014-04, RWTH Aachen, February 2014. Revised version.
[ pdf | http ]

In the theory of deterministic automata for languages of infinite words, a fundamental fact relates the family of infinitary limits of regular languages and the family of omega-languages recognized by deterministic Büchi automata. With the known definitions of asynchronous automata, this observation does not extend to the context of traces. A major difficulty is posed by processes that stall after finitely many transitions. We introduce the family of deterministic, synchronization-aware asynchronous automata which - using as parameter the set of processes that stay live ad infinitum - allows us to settle an open question, namely, whether there exists a deterministic Büchi automaton recognizing precisely the infinitary limit of a regular trace language. Also, the corresponding class of unparameterized Muller automata captures all trace languages.

[CG14b] Namit Chaturvedi and Marcus Gelderie. Weak omega-Regular Trace Languages. arXiv.org, Feb 2014. CoRR abs/1402.3199.
[ pdf | http ]

Mazurkiewicz traces describe concurrent behaviors of distributed systems. Trace-closed word languages, which are linearizations of trace languages, constitute a weaker notion of concurrency but still give us tools to investigate the latter. In this vein, our contribution is twofold. Firstly, we develop definitions that allow classification of omega-regular trace languages in terms of the corresponding trace-closed omega-regular word languages, capturing E-recognizable (reachability) and (deterministically) Büchi recognizable languages. Secondly, we demonstrate the first automata-theoretic result that shows the equivalence of omega-regular trace-closed word languages and Boolean combinations of deterministically I-diamond Büchi recognizable trace-closed languages.

[Fel14] Ingo Felscher. Model composition in model-checking. PhD thesis, RWTH Aachen, 2014.
[ pdf | http ]

Model-checking allows one to formally check properties of systems: these properties are modeled as logic formulas and the systems as structures like transition systems. These transition systems are often composed, i.e., they arise in form of products or sums. The composition technique allows us to deduce the truth of a formula in the composed system from ``interface information'': the truth of formulas for the component systems and information in which components which of these formulas hold. We are interested in identifying situations where the composition technique works in the context of model-checking (reachability properties, linear and branching time temporal logic) and, in these cases, how large the interface information can become. In the first main part of this thesis, we extend known results for synchronized products of transition systems by showing a composition theorem for finitely synchronized products and first-order logic (or modal logic) extended by regular reachability over a unary alphabet. We further show that the composition technique fails for two generalizations of the logic: in the general case of regular reachability and in the case of propositional dynamic logic over a unary alphabet. Furthermore, it fails for synchronized products which are not finitely synchronized. A known drawback of the composition technique is the growth of the size of the generated interface information in relation to the given formula. Göller, Jung and Lohrey have shown a non-elementary lower bound for this size in general for first-order logic (for products) and modal logic (for disjoint ordered sums). In the second and third part of this thesis, we look at combinations of logics and systems where we can avoid this. In the second part, we show a composition theorem for linear temporal logic (LTL) and disjoint ordered sums of words. A careful analysis shows that, here, the size of the interface information only grows at most exponential in the size of the given formula. In the third part, we generalize this composition technique to a disjoint ordered sum of trees and computation tree logic (CTL). Here, we deal with trees as components which are composed via a tree structure. We show a composition result for which the interface information grows exponentially in the size of the given formula and in the branching of the index tree structure.

2013

[Brü13] Benedikt Brütsch. Synthesizing structured reactive programs via deterministic tree automata. In Fabio Mogavero, Aniello Murano, and Moshe Y. Vardi, editors, Proceedings 1st International Workshop on Strategic Reasoning, volume 112 of Electronic Proceedings in Theoretical Computer Science, pages 107-113. Open Publishing Association, 2013.
[ pdf | http ]

Existing approaches to the synthesis of reactive systems typically involve the construction of transition systems such as Mealy automata. However, in order to obtain a succinct representation of the desired system, structured programs can be a more suitable model. In 2011, Madhusudan proposed an algorithm to construct a structured reactive program for a given omega-regular specification without synthesizing a transition system first. His procedure is based on two-way alternating omega-automata on finite trees that recognize the set of correct programs. We present a more elementary and direct approach using only deterministic bottom-up tree automata that compute so-called signatures for a given program. In doing so, we extend Madhusudan's results to the wider class of programs with bounded delay, which may read several input symbols before producing an output symbol (or vice versa). As a formal foundation, we inductively define a semantics for such programs.

[Fri13] W. Fridman. A study of pushdown games. PhD thesis, RWTH Aachen, 2013.
[ pdf | http ]

Infinite two-player games are of interest in computer science since they provide an algorithmic framework for the study of nonterminating reactive systems. Usually, an infinite game is specified by an ω-language containing all winning plays for one of the two players or by a game graph and a winning condition on infinite paths through this graph. Many algorithmic results are known for the case of regular specifications and for finite game graphs with winning conditions like parity or Muller conditions capturing regular objectives. The present thesis offers results that also cover a class of nonregular specifications as well as a class of infinite game graphs, namely those specified by pushdown automata, i.e, we consider contextfree specifications and pushdown game graphs with parity or Muller winning conditions. We extend various central results known for regular games to the class of pushdown games. We focus on the following four questions. Firstly, we analyze how the format of a pushdown winning strategy matches the type of the pushdown game specification. Here, we establish a strong connection between the formats of specifications and formats of corresponding winning strategies for several types of contextfree games, but we also exhibit cases of contextfree games where this correspondence fails. Secondly, we investigate delay games with contextfree winning conditions. In such a game one of the players has the possibility to postpone his moves for some time, thus obtaining a lookahead on the moves of the opponent. We clarify whether the winner of a deterministic contextfree delay game can be determined effectively as well as what amount of lookahead is necessary to win such games. Thirdly, we investigate the synthesis problem for distributed systems which consist of several cooperating components communicating with each other and with the environment. A distributed system is specified by an architecture comprising the communication structure of the system. Here, we study both main concepts, that of global and that of local specifications. We offer a complete characterization of the decidable architectures for local specifications, which may be deterministic contextfree or regular. Moreover, we prove that, for global deterministic contextfree specifications, the distributed synthesis problem is undecidable. Finally, we address the problem whether the winner of an infinite game can be already determined after a finite play prefix. Extending results for the case of finite game graphs, we introduce finite-duration parity pushdown games and establish their completeness for solving parity pushdown games. This yields a new reduction method to determine the winner of a pushdown game by solving a reachability game on a finite game graph.

[GLMN13b] Pranav Garg, Christof Löding, P. Madhusudan, and Daniel Neider. Learning universally quantified invariants of linear data structures. In Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, volume 8044 of Lecture Notes in Computer Science, pages 813-829. Springer, 2013.
[ pdf ]

We propose a new automaton model, called quantified data automata over words, that can model quantified invariants over linear data structures, and build poly-time active learning algorithms for them, where the learner is allowed to query the teacher with membership and equivalence queries. In order to express invariants in decidable logics, we invent a decidable subclass of QDAs, called elastic QDAs, and prove that every QDA has a unique minimally-over-approximating elastic QDA. We then give an application of these theoretically sound and efficient active learning algorithms in a passive learning framework and show that we can efficiently learn quantified linear data structure invariants from samples obtained from dynamic runs for a large class of programs.

[GLMN13a] Pranav Garg, Christof Löding, P. Madhusudan, and Daniel Neider. ICE: A Robust Learning Framework for Synthesizing Invariants. Technical report, RWTH Aachen University and University of Illinois at Urbana-Champaign, 2013.
[ pdf ]

We introduce a new paradigm for using black-box learning to synthesize invariants called ICE-learning that learns using examples, counter-examples, and implications, and show that it allows building honest teachers and convergent mechanisms for invariant synthesis. We observe that existing algorithms for black-box abstract interpretation can be interpreted as monotonic ICE learning algorithms, develop two classes of new non-monotonic ICE-learning domains, one for learning numerical invariants for scalar variables and one for quantified invariants for arrays and dynamic lists, and establish convergence results for them. We implement these ICE learning algorithms in a prototype verifier and show that the robustness that it brings is practical and effective.

[Gel13] Marcus Gelderie. Strategy composition in compositional games. In Fedor V. Fomin, Rusins Freivalds, Marta Kwiatkowska, and David Peleg, editors, Automata, Languages and Programming, Lecture Notes in Computer Science, 2013.
[ pdf | http ]
[LL13] Martin Lang and Christof Löding. Modeling and verification of infinite systems with resources. Logical Methods in Computer Science, 9(4), 2013.
[ pdf ]

We consider formal verification of recursive programs with resource consumption. We introduce prefix replacement systems with non-negative integer counters which can be incremented and reset to zero as a formal model for such programs. In these systems, we investigate bounds on the resource consumption for reachability questions. Motivated by this question, we introduce relational structures with resources and a quantitative first-order logic over these structures. We define resource automatic structures as a subclass of these structures and provide an effective method to compute the semantics of the logic on this subclass. Subsequently, we use this framework to solve the bounded reachability problem for resource prefix replacement systems. We achieve this result by extending the well-known saturation method to annotated prefix replacement systems. Finally, we provide a connection to the study of the logic cost-WMSO.

[LR13] Christof Löding and Stefan Repke. Decidability Results on the Existence of Lookahead Delegators for NFA. In Anil Seth and Nisheeth K. Vishnoi, editors, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013), volume 24 of Leibniz International Proceedings in Informatics (LIPIcs), pages 327-338, Dagstuhl, Germany, 2013. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.
[ pdf | http ]

In this paper, we study lookahead delegators for nondeterministic finite automata (NFA), which are functions that deterministically choose transitions by additionally using a bounded lookahead on the input word. Of course, the delegator has to lead to an accepting state for each word that is accepted by the NFA. In the special case where no lookahead is allowed, a delegator coincides with a deterministic transition function that preserves the language. Typical decision problems are to decide whether a delegator with a given fixed lookahead exists, or whether a delegator with some bounded lookahead exists for a given NFA. In a paper of Ravikumar and Santean from 2007, the complexity and decidability of these questions have been tackled, mainly for the case of unambiguous NFA. In this paper, we revisit the subject and provide results for the case of general NFA. First, we correct a complexity result from the above paper by showing that the existence of delegators with fixed lookahead can be decided in time polynomial in the number of states. We use two player games on graphs as a tool to obtain the result. As second contribution, we show that the problem becomes PSPACE-complete if the bound on the lookahead is a part of the input. The third result provides a bound on the maximal required amount of lookahead. We use this to show that the (previously open) problem of deciding the existence of a bounded lookahead delegator is also PSPACE-complete.

[NJ13] Daniel Neider and Nils Jansen. Regular Model Checking Using Solver Technologies and Automata Learning. In Proceedings of the 5th International NASA Formal Methods Symposium (NFM 2013), volume 7871 of Lecture Notes in Computer Science, pages 16-31. Springer, 2013.
[ pdf ]

Regular Model Checking is a popular verification technique where large and even infinite sets of program configurations can be encoded symbolically by finite automata. Thereby, the handling of regular sets of initial and bad configurations often imposes a serious restriction in practical applications. We present two new algorithms both utilizing modern solver technologies and automata learning. The first one works in a CEGAR-like fashion by iteratively refining an abstraction of the reachable state space using counterexamples, while the second one is based on Angluin’s prominent learning algorithm. We show the feasibility and competitiveness of our approaches on different benchmarks and compare them to other established tools.

[Zim13] M. Zimmermann. Optimal Bounds in Parametric LTL Games. Theoretical Computer Science, 493:30-45, 2013. Journal version of [Zim11]. (c) Elsevier.
[ pdf | ps ]

Parameterized linear temporal logics are extensions of Linear Temporal Logic (LTL) by temporal operators equipped with variables that bound their scope. In model-checking, such specifications were introduced as PLTL by Alur et al. and as PROMPT-LTL by Kupferman et al. We show how to determine in doubly-exponential time, whether a player wins a game with PLTL winning condition with respect to some, infinitely many, or all variable valuations. Hence, these problems are not harder than solving LTL games. Furthermore, we present an algorithm with triply-exponential running time to determine optimal variable valuations that allow a player to win a game. Finally, we give doubly-exponential upper and lower bounds on the values of such optimal variable valuations.

2012

[BLO12] Stefan Breuers, Christof Löding, and Jörg Olschewski. Improved Ramsey-based Büchi complementation. In FoSSaCS 2012, volume 7213 of Lecture Notes in Computer Science, pages 150-164. Springer, 2012. (c) Springer.

We consider complementing Büchi automata by applying the Ramsey-based approach, which is the original approach already used by Büchi and later improved by Sistla et al. We present several heuristics to reduce the state space of the resulting complement automaton and provide experimental data that shows that our improved construction can compete (in terms of finished complementation tasks) also in practice with alternative constructions like rank-based complementation. Furthermore, we show how our techniques can be used to improve the Ramsey-based complementation such that the asymptotic upper bound for the resulting complement automaton is 2O(n log n) instead of 2O(n^2).

[CMDC12] N. Chaturvedi, B. Meenakshi, and A. Datta Chowdhury. A framework for decentralized access control using finite state automata. In Deepak D'Souza and Priti Shankar, editors, Modern Applications of Automata Theory, volume 2 of IISc Research Monographs Series, pages 171-191. World Scientific, May 2012.
[ http ]

We present a decentralized authorization framework for physical access control, using finite state automata on a system of networked controllers and smart cards. Access to individual rooms is guarded by context-dependent policies that are dynamically evaluated. Policies are specified using a logical language parameterized by events which are then converted into equivalent executable automata. Storage and evaluation of policy automata is done in a distributed manner. We include illustrative examples of context sensitive physical access control policies that are derived from actual applications.

[COT12] N. Chaturvedi, J. Olschewski, and W. Thomas. Languages vs. omega-languages in regular infinite games. International Journal of Foundations of Computer Science, 23(05):985-1000, August 2012. Journal version of [COT11]. (c) 2012 World Scientific Publishing Company.
[ pdf | http ]

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.

[FZ12a] J. Fearnley and M. Zimmermann. Playing Muller Games in a Hurry. International Journal of Foundations of Computer Science, 23:649-668, 2012. Journal version of [FZ10]. International Journal of Foundations of Computer Science (c) 2012 World Scientific Publishing Company.
[ pdf | ps ]

This work considers a finite-duration variant of Muller games, and their connection to infinite-duration Muller games. In particular, it studies the question of how long a finite- duration Muller game must be played before the winner of the finite-duration game is guaranteed to be able to win the corresponding infinite-duration game. Previous work by McNaughton has shown that this must occur after Pij=1n(j!+1) moves, and the reduction from Muller games to parity games gives a bound of n· n!+ 1 moves. We improve upon both of these results, by giving a bound of 3n moves.

[Fel12] I. Felscher. LTL-Model-Checking via Model Composition. In Alain Finkel, Jerome Leroux, and Igor Potapov, editors, Reachability Problems, 6th International Workshop, RP 2012, Bordeaux, France, September 17-19, 2012. Proceedings, volume 7550 of Lecture Notes in Computer Science, pages 42-53. Springer, 2012.
[ pdf | http ]

We develop a composition technique for linear time logic (LTL) over ordered disjoint sums of words. This technique allows to reduce the validity of an LTL formula in the sum to LTL formulas over the components. It is known that for first order logic (FO) and even its three variable fragment FO^3 the number of formulas generated for the components is at least non-elementary in the size of the input formula. We show that for LTL – expressively equivalent to FO logic – over an ordered disjoint sum of words the number of formulas for the components can be kept at an at most exponential growth in the size of the input formula.

[FZ12b] W. Fridman and M. Zimmermann. Playing Pushdown Parity Games in a Hurry. In M. Faella and A. Murano, editors, Proceedings of the Third International Symposium on Games, Automata, Logic, and Formal Verification, GandALF 2012, volume 96 of Electronic Proceedings in Theoretical Computer Science, pages 183-196, 2012.
[ pdf | ps ]

We continue the investigation of finite-duration variants of infinite-duration games by extending known results for games played on finite graphs to those played on infinite ones. In particular, we establish an equivalence between pushdown parity games and a finite-duration variant. This allows us to determine the winner of a pushdown parity game by solving a reachability game on a finite tree.

[Gel12a] M. Gelderie. Strategy machines and their complexity (with addendum). Technical Report AIB-2012-04, RWTH-Aachen, 2012.
[ pdf ]
[Gel12b] Marcus Gelderie. Strategy machines and their complexity (with addendum). In Branislav Rovan, Vladimiro Sassone, and Peter Widmayer, editors, Mathematical Foundations of Computer Science 2012, volume 7464 of Lecture Notes in Computer Science, pages 431-442. Springer Berlin / Heidelberg, 2012. 10.1007/978-3-642-32589-2_39.
[ pdf | http ]
[GRT12] Sten Grüner, Frank G. Radmacher, and Wolfgang Thomas. Connectivity games over dynamic networks. Theoretical Computer Science, 2012. Extended version of [RT07b] and [GRT11]. (c) Elsevier.
[ pdf ]

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.

[IL12] Dimitri Isaak and Christof Löding. Efficient inclusion testing for simple classes of unambiguous omega-automata. Information Processing Letters, 112(14-15):578-582, 2012.
[ pdf | http ]

We show that language inclusion for languages of infinite words defined by nondeterministic automata can be tested in polynomial time if the automata are unambiguous and have simple acceptance conditions, namely safety or reachability conditions. An automaton with safety condition accepts an infinite word if there is a run that never visits a forbidden state, and an automaton with reachability condition accepts an infinite word if there is a run that visits an accepting state at least once.

[LN12] Martin Leucker and Daniel Neider. Learning Minimal Deterministic Automata from Inexperienced Teachers. In Proceedings of the 5th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2012), volume 7609 of Lecture Notes in Computer Science, pages 524-538. Springer, 2012.
[ pdf ]

A prominent learning algorithm is Angluin's L* algorithm, which allows to learn a minimal deterministic automaton using so-called membership and equivalence queries addressed to a teacher. In many applications, however, a teacher might be unable to answer some of the membership queries because parts of the object to learn are not completely specified, not observable, it is too expensive to resolve these queries, etc. Then, these queries may be answered inconclusively. In this paper, we survey different algorithms to learn minimal deterministic automata in this setting in a coherent fashion. Moreover, we provide modifications and improvements for these algorithms, which are enabled by recent developments.

[Löd12] C. Löding. Basics on tree automata. In Deepak D'Souza and Priti Shankar, editors, Modern Applications of Automata Theory. World Scientific, 2012.
[LR12] Christof Löding and Stefan Repke. Regularity Problems for Weak Pushdown omega-Automata and Games. In Branislav Rovan, Vladimiro Sassone, and Peter Widmayer, editors, Mathematical Foundations of Computer Science 2012, volume 7464 of Lecture Notes in Computer Science, pages 764-776. Springer Berlin / Heidelberg, 2012. 10.1007/978-3-642-32589-2_66.
[ pdf | http ]

We show that the regularity and equivalence problems are decidable for deterministic weak pushdown omega-automata, giving a partial answer to a question raised by Cohen and Gold in 1978. We prove the decidability by a reduction to the corresponding problems for determinis- tic pushdown automata on finite words. Furthermore, we consider the problem of deciding for pushdown games whether a winning strategy exists that can be implemented by a finite automaton. We show that this problem is already undecidable for games defined by one-counter automata or visibly pushdown automata with a safety condition.

[Nei12] Daniel Neider. Computing Minimal Separating DFAs and Regular Invariants Using SAT and SMT Solvers. In Proceedings of the 10th International Symposium on Automated Technology for Verification and Analysis (ATVA 2012), volume 7561 of Lecture Notes in Computer Science, pages 354-369. Springer, 2012.
[ pdf ]

We develop a generic technique to compute minimal separating DFAs (deterministic finite automata) and regular invariants. Our technique works by expressing the desired properties of a solution in terms of logical formulae and using SAT or SMT solvers to find solutions. We apply our technique to three concrete problems: computing minimal separating DFAs (e.g., used in compositional verification), regular model checking, and synthesizing loop invariants of integer programs that are expressible in Presburger arithmetic.

[NRZ12] D. Neider, R. Rabinovich, and M. Zimmermann. Down the Borel Hierarchy: Solving Muller Games via Safety Games. In M. Faella and A. Murano, editors, Proceedings of the Third International Symposium on Games, Automata, Logic, and Formal Verification, GandALF 2012, volume 96 of Electronic Proceedings in Theoretical Computer Science, pages 169-182, 2012.
[ pdf | ps ]

We transform a Muller game with n vertices into a safety game with (n!)^3 vertices whose solution allows to determine the winning regions of the Muller game and to compute a finite-state winning strategy for one player. This yields a novel antichain-based memory structure and a natural notion of permissive strategies for Muller games. Moreover, we generalize our construction by presenting a new type of game reduction from infinite games to safety games and show its applicability to several other winning conditions.

[Rad12] Frank G. Radmacher. Games on dynamic networks: Routing and connectivity. PhD thesis, RWTH Aachen, 2012.
[ pdf ]

Infinite games are a strong model for analyzing dynamic networks that encounter continuous topological changes during operation. In this framework, the players represent the contrary forces which modify the network. In particular, this thesis deals with three different two-player games which focus on guaranteeing routing and connectivity properties in dynamic networks. In each model, one player has to establish the proper operation of the network, while the adversary produces failures and demands that occur during operation. In the first part, we study sabotage games, which van Benthem introduced in 2002. In these games, a Runner traverses a graph and tries to reach a set of goal vertices, while a Blocker removes edges. We refine this game in two ways; namely we consider a more general winning objective expressed in linear temporal logic, and we study the variant in which Blocker is replaced by a probabilistic player. We show that in both cases the problem to decide whether Runner wins remains PSPACE-complete. In the second part, we develop a routing game in which a routing agent has to deliver packets to their destinations, while a demand agent continuously generates packets and blocks connections for a certain amount of time. We show general limitations for obtaining routing strategies but also point to algorithmic solutions. The results depend on both the desired routing property and the coarseness of the model. For certain scenarios we develop feasible routing algorithms, each of which guarantees a routing property against any behavior of the demand agent. In the third part, we introduce a connectivity game between a Constructor and a Destructor. While Destructor deletes nodes, Constructor can restore or even create new nodes under certain conditions. Also, we model information flow through the network by allowing Constructor to change labels of adjacent nodes. Constructor either has a reachability or a safety objective, i.e., Constructor has to either establish a connected network or guarantee that the network always stays connected. We show under what conditions the solvability of these games is decidable and, in this case, analyze the computational complexity. The results depend on the abilities of Constructor and differ for the reachability and the safety version.

[Sla12] Michaela Slaats. Infinite regular games in the higher-order pushdown and the parametrized setting. PhD thesis, RWTH Aachen, 2012.
[ pdf | http ]

Higher-order pushdown systems extend the idea of pushdown systems by using a ``higher-order stack'' (which is a nested stack). More precisely on level 1 this is a standard stack, on level 2 it is a stack of stacks, and so on. We study the higher-order pushdown systems in the context of infinite regular games. In the first part, we present a k-ExpTime algorithm to compute global positional winning strategies for parity games which are played on the configuration graph of a level-k higher-order pushdown system. To represent those winning strategies in a finite way we use a notion of regularity for sets of higher-order stacks that relies on certain (``symmetric'') operations to build higher-order stacks. The construction of the strategies is based on automata theoretic techniques and uses the fact that the higher-order stacks constructed by symmetric operations can be arranged uniquely in a tree structure. In the second part, we study the solution of games in the sense of Gale and Stewart where the winning condition is specified by an MSO-formula varphi(P) with a parameter PN. This corresponds to a three player game where the i-th round between the two original players is extended by the choice of the bit 1 or 0 depending on whether iin P or not. We consider the case that the parameter can be constructed by some deterministic machine, a ``parameter generator''. We solve the parametrized regular games for parameters P given by two kinds of such generators, namely: higher-order pushdown automata and collapsible pushdown automata. In the third part, we study higher-order pushdown systems and higher-order counter systems (where the stack alphabet contains only one symbol), by comparing the language classes accepted by corresponding automata. For example, we show that level-k pushdown languages are level-(k+1) counter languages.

[WGLW12] E. Weingaertner, R. Glebke, M. Lang, and K. Wehrle. Building a modular bittorrent model for ns-3. In Proceedings of the 2012 workshop on ns-3 (WNS3 2012), 3 2012.

Over the past decade BitTorrent has established itself as the virtual standard for P2P file sharing in the Internet. However, it is currently not possible to investigate BitTorrent with ns-3 due to the unavailability of an according application model. In this paper we eliminate this burden. We present a highly modular BitTorrent model which allows for the easy simulation of different BitTorrent systems such as file sharing as well as present and future BitTorrent-based Video-on-Demand systems.

[Zim12] M. Zimmermann. Solving Infinite Games with Bounds. PhD thesis, RWTH Aachen University, 2012.
[ pdf ]

We investigate the existence and the complexity of computing and implementing optimal winning strategies for graph games of infinite duration.

Parameterized linear temporal logics are extensions of Linear Temporal Logic (LTL) by temporal operators equipped with variables for time bounds. In model-checking, such specifications were introduced as PLTL by Alur et al. and as PROMPT-LTL by Kupferman et al. We show how to determine in doubly-exponential time, whether a player wins a game with PLTL winning condition with respect to some, infinitely many, or all variable valuations. Hence, these problems are not harder than solving LTL games. Furthermore, we present an algorithm with triply-exponential running time to determine optimal variable valuations that allow a player to win a game. Finally, we give doubly-exponential upper and lower bounds on the values of optimal variable valuations.

In Muller games, we measure the quality of a winning strategy using McNaughton's scoring functions. We construct winning strategies that bound the losing player's scores by two and show this to be optimal. This improves the previous best upper bound of n! in a game with n vertices, obtained by McNaughton. Using these strategies, we show how to transform a Muller game into a safety game whose solution allows to determine the winning regions of the Muller game and to compute a finite-state winning strategy for one player. This yields a novel antichain-based memory structure and the first definition of permissive strategies for Muller games. Moreover, we generalize our construction by presenting a new type of game reduction from infinite games to safety games and show its applicability to several other winning conditions.

2011

[BMOU11] Patricia Bouyer, Nicolas Markey, Jörg Olschewski, and Michael Ummels. Measuring permissiveness in parity games: Mean-payoff parity games revisited. In Automated Technology for Verification and Analysis, volume 6996 of Lecture Notes in Computer Science, pages 135-149. Springer, 2011. (c) Springer.

We study nondeterministic strategies in parity games with the aim of computing a most permissive winning strategy. Following earlier work, we measure permissiveness in terms of the average number/weight of transitions blocked by a strategy. Using a translation into mean-payoff parity games, we prove that deciding (the permissiveness of) a most permissive winning strategy is in NP and coNP. Along the way, we provide a new study of mean-payoff parity games. In particular, we give a new algorithm for solving these games, which beats all previously known algorithms for this problem.

[COT11] N. Chaturvedi, J. Olschewski, and W. Thomas. Languages vs. omega-languages in regular infinite games. In Giancarlo Mauri and Alberto Leporati, editors, Proceedings of the 15th International Conference on Developments in Language Theory, DLT 2011, volume 6795 of Lecture Notes in Computer Science, pages 180-191. Springer, 2011.
[ pdf | http ]

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.

[FT11b] I. Felscher and W. Thomas. On Compositional Failure Detection in Structured Transition Systems. Technical Report AIB-2011-12, RWTH Aachen University, 2011. Full version of [FT11a].
[ pdf | .ps.gz ]

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.

[FT11a] I. Felscher and W. Thomas. Compositional failure detection in structured transition systems. In Implementation and Application of Automata, 16th International Conference, CIAA 2011, Blois, France, July 13-16, 2011. Proceedings, volume 6807 of Lecture Notes of Computer Science, pages 130-141, 2011.
[ http ]

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.

[FLZ11] W. Fridman, C. Löding, and M. Zimmermann. Degrees of Lookahead in Context-free Infinite Games. In Marc Bezem, editor, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL, volume 12 of Leibniz International Proceedings in Informatics (LIPIcs), pages 264-276, Dagstuhl, Germany, 2011. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.
[ pdf | ps | http ]

We continue the investigation of delay games, infinite games in which one player may postpone her moves for some time to obtain a lookahead on her opponent's moves. We show that the problem of determining the winner of such a game is undecidable for deterministic context-free winning conditions. Furthermore, we show that the necessary lookahead to win a deterministic context-free delay game cannot be bounded by any elementary function. Both results hold already for restricted classes of deterministic context-free winning conditions.

[FP11] W. Fridman and B. Puchala. Distributed Synthesis for Regular and Contextfree Specifications. In Proceedings of the 36th International Symposium on Mathematical Foundations of Computer Science, MFCS 2011, Lecture Notes in Computer Science. Springer, 2011.
[ pdf ]

We adress the controller synthesis problem for distributed systems with regular and deterministic contextfree specifications. Our main result is a complete characterization of the decidable architectures for local specifications. This extends existing results on local specifications in two directions. First, we consider arbitrary, not necessarily acyclic, architectures and second, we allow deterministic contextfree specifications.Moreover, we show that as soon as one considers global deterministic contextfree specifications, even very simple architectures are undecidable.

[Gel11a] M. Gelderie. Classifying regular languages via cascade products of automata. Diploma Thesis (revised version), RWTH Aachen, 2011.
[ pdf ]
[Gel11b] Marcus Gelderie. Classifying regular languages via cascade products of automata. In Adrian-Horia Dediu, Shunsuke Inenaga, and Carlos Martín-Vide, editors, Language and Automata Theory and Applications, volume 6638 of Lecture Notes in Computer Science, pages 286-297. Springer Berlin / Heidelberg, 2011. The original publication is available at www.springerlink.com.
[ pdf | http ]
[GH11] Marcus Gelderie and Michael Holtmann. Memory reduction via delayed simulation. In Johannes Reich and Bernd Finkbeiner, editors, Proceedings International Workshop on Interactions, Games and Protocols Saarbrücken, Germany, 27th March 2011, volume 50 of Electronic Proceedings in Theoretical Computer Science, pages 46-60. Open Publishing Association, February 2011.
[GRT11] Sten Grüner, Frank G. Radmacher, and Wolfgang Thomas. Connectivity games over dynamic networks. In Proceedings of the 2nd International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2011, volume 54 of Electronic Proceedings in Theoretical Computer Science, pages 131-145, 2011.
[ pdf ]

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.

[Hol11] Michael Holtmann. Memory and delay in regular infinite games. PhD thesis, RWTH Aachen, 2011.
[ pdf | http ]

Infinite two-player games constitute a powerful and flexible framework for the design and verification of reactive systems. It is well-known that, for example, the construction of a controller acting indefinitely within its environment can be reduced to the computation of a winning strategy in an infinite game (Pnueli and Rosner, 1989). For the class of regular games, Büchi and Landweber (1969) showed that one of the players has a winning strategy which can be realized by a finite-state automaton. Based on this fundamental result, many efforts have been made by the research community to improve the solution methods for infinite games. This is meant with respect to both the time needed to compute winning strategies and the amount of space required to implement them. In the present work we are mainly concerned with the second aspect. We study two problems related to the construction of small controller programs. In the first part of the thesis, we address the classical problem of computing finite-state winning strategies which can be realized by automata with as little memory, i.e., number of states, as possible. Even though it follows from a result of Dziembowski et al. (1997) that there exist exotic regular games for which the size of automata implementing winning strategies is at least exponential in the size of the game arena, most practical cases require far less space. We propose an efficient algorithm which reduces the memory used for the implementation of winning strategies, for several classes of regular conditions, and we show that our technique can effect an exponential gain in the size of the memory. In the second part of this thesis, we introduce a generalized notion of a strategy. One of the players is allowed to delay each of his moves for a finite number of steps, or, in other words, exploit in his strategy some lookahead on the moves of the opponent. This setting captures situations in distributed systems, for example, when buffers are present in communication between remote components. Our concept of strategies corresponds to the class of continuous operators, thereby extending the work of Hosch and Landweber (1972) and, in particular, that of Büchi and Landweber (1969). We show that the problem whether a given regular specification is solvable by a continuous operator is decidable and that each continuous solution can be reduced to one of bounded lookahead. From our results, we derive a generalized determinacy of regular conditions.

[Lan11] M. Lang. Resource-bounded Reachability on Pushdown Systems. Master thesis, RWTH Aachen, 2011.
[ pdf ]

In this work, we combine the theory of pushdown systems and the theory of resource automata (also known as B-automata) to a model which we call resource pushdown systems. This model can be seen as pushdown system with resource counters which support the operations increment, reset to zero and no-change. The pushdown rules are annotated with these counter operations. Resource prefix replacement systems can be used to model recursive programs with resource consumption. We consider bounded reachability as a natural extension of the normal reachability in the presence of resources. A set of pushdown configurations B is called boundedly reachable from another set A if there is finite resource-bound k in N such that for all configurations from A, it is possible to reach some configuration in B with a resource usage of at most k. We prove the decidability of the bounded reachability problem in the slightly more general scenario of resource prefix replacement systems and regular sets of configurations A and B. This result is achieved by an extension of saturation algorithms. We establish a direct correspondence between the saturated automaton and the resource-cost of reachability. In the following, we use the known decidability of the boundedness problem for resource automata to solve the bounded reachability problem. Moreover, we investigate alternating reachability in form of resource reachability games. We show that these games are positionally determined in the case of one resource counter without resets. We introduce the bounded winning problem as a variant of the bounded reachability problem in games. Subsequently, we prove the decidability of this problem for resource reachability games on pushdown graphs with one resource counter and without reset. Finally, we introduce the logic FO+RR which allows to express specifications in systems with resources. This logic is evaluated over structures whose relations need a specific amount of resources in order to be satisfied. The syntax of FO+RR mostly resembles first-order logic without negation. The semantics of a formula is given by the minimal amount of resources which are needed to satisfy the formula with respect to all relations. In analogy to the idea of automatic structures, we introduce the concept of resources automatic structures and prove that the FO+RR semantics on these structures is effectively computable.

[Löd11] C. Löding. Infinite games and automata theory. In Krzysztof R. Apt and Erich Grädel, editors, Lectures in Game Theory for Computer Scientists. Cambridge University Press, 2011.
[Nei11] Daniel Neider. Small Strategies for Safety Games. In Proceedings of the 9th Symposium on Automated Technology for Verification and Analysis (ATVA 2011), volume 6996 of Lecture Notes in Computer Science, pages 306-320. Springer, 2011.
[ pdf ]

We consider safety games on finite, edge-labeled graphs and present an algorithm based on automata learning to compute small strategies. Our idea is as follows: we incrementally learn regular sets of winning plays until a winning strategy can be derived. For this purpose we develop a modified version of Kearns and Vazirani’s learning algorithm. Since computing a minimal strategy in this setting is hard (we prove that the corresponding decision problem is NP-complete), our algorithm, which runs in polynomial time, is an interesting and effective heuristic that yields small strategies in our experiments.

[NRZ11] D. Neider, R. Rabinovich, and M. Zimmermann. Solving Muller Games via Safety Games. Technical Report AIB-2011-14, RWTH Aachen, 2011.
[ pdf | ps ]

We show how to transform a Muller game with n vertices into a safety game with (n!)^3 vertices whose solution allows to determine the winning regions of the Muller game and a winning strategy for one player.

[STW11] Alex Spelten, Wolfgang Thomas, and Sarah Winter. Trees over infinite structures and path logics with synchronization. In Fang Yu and Chao Wang, editors, Proceedings of the 13th International Workshop on Verification of Infinite-State Systems, volume 73 of EPTCS, pages 20-34, 2011.
[ pdf ]

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.

[Tho11] W. Thomas. Infinite games and uniformization. In M. Banerjee and A. Seth, editors, Proceedings of the 4th Indian Conference on Logic and Its Applications, ICLA 2011, volume 6521 of Lecture Notes in Computer Science, pages 19-21. Springer, 2011. (c) Springer.
[ pdf ]

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.

[Zim11] M. Zimmermann. Optimal Bounds in Parametric LTL Games. In G. D'Agostino and S. La Torre, editors, Proceedings of the Second International Symposium on Games, Automata, Logic, and Formal Verification, GandALF 2011, volume 54 of Electronic Proceedings in Theoretical Computer Science, pages 146-161, 2011. Note: the proof of Theorem 10 contains an error. The journal version [Zim13] presents a 3EXPTIME algorithm for the optimization problems. See also Chapter 3 of my PhD thesis [Zim12].
[ pdf | ps ]

We consider graph games of infinite duration with winning conditions in parameterized linear temporal logic, where the temporal operators are equipped with variables for time bounds. In model checking such specifications were introduced as PLTL by Alur et al. and (in a different version called PROMPT-LTL) by Kupferman et al..

We present an algorithm to determine optimal variable valuations that allow a player to win a game. Furthermore, we show how to determine whether a player wins a game with respect to some, infinitely many, or all valuations. All our algorithms run in doubly-exponential time; so, adding bounded temporal operators does not increase the complexity compared to solving plain LTL games.

2010

[Alt10] J. Altenbernd. Reachability over word rewriting systems. PhD thesis, RWTH Aachen, 2010.
[ pdf | http ]

Word rewriting systems have been studied over the last century under several aspects. In the beginning, they were considered as a framework for the representation of computation processes and as a tool for generating formal languages. In more recent years, they have also been investigated as a mechanism to represent infinite graphs by a finite formalism. This thesis has its main focus in the latter domain. In the first part of the thesis, we investigate mixed prefix/suffix rewriting (MPSR) systems, which combine prefix and suffix rewriting in a nondeterministic way. We study central algorithmic properties of the graphs that can be generated by such systems, with an emphasis on the reachability problem (as a master problem in model-checking), and we determine the connection between the classes of such graphs and other well-studied graph classes, such as the classes of prefix recognizable and of automatic graphs. Furthermore, we study the class of trace languages of graphs that are generated by MPSR systems, and we show that this class strictly includes the class of context-free languages, and is itself properly included in the class of context-sensitive languages. In the second part of the thesis, we introduce and investigate tagged infix rewriting (TIR) systems, which extend the MPSR systems, and which use special markers for a restricted form of infix rewriting. We show that in their basic form, where the markers may not be rewritten, TIR and MPSR systems share a number of model-checking properties, and we obtain analogous results concerning their trace languages. We also study two variants of TIR systems. For the first, where markers may be removed by rewriting steps, we show that such systems preserve regularity of languages under rewriting, by adapting the saturation method as known for pushdown systems. In the second variant, where markers may be added by rewriting steps, this does not hold; however, we show that an algorithmic reachability analysis is still possible.

[BKK+10] Benedikt Bollig, Joost-Pieter Katoen, Carsten Kern, Martin Leucker, Daniel Neider, and David R. Piegdon. libalf: The Automata Learning Framework. In Proceedings of the 22nd International Conference on Computer Aided Verification (CAV 2010), volume 6174 of Lecture Notes in Computer Science, pages 360-364. Springer, 2010.
[ pdf ]

This paper presents libalf, a comprehensive, open-source library for learning formal languages. libalf covers various well-known learning techniques for finite automata (e.g. Angluin's L*, Biermann, RPNI etc.) as well as novel learning algorithms (such as for NFA and visibly one-counter automata). libalf is flexible and allows facilely interchanging learning algorithms and combining domain-specific features in a plug-and-play fashion. Its modular design and C++ implementation make it a suitable platform for adding and engineering further learning algorithms for new target models (e.g., Büchi automata).

[BSA+10] K. Bollue, M. Slaats, E. Abraham, W. Thomas, and D. Abel. Synthesis of Behavioral Controllers for DES: Increasing Efficiency. In 10th Int. Workshop on Discrete-Event Systems (WODES'10), IFAC, pages 30-37, 2010.
[ pdf ]

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.

[BL10] Nicolas Bousquet and Christof Löding. Equivalence and inclusion problem for strongly unambiguous Büchi automata. In 4th International Conference on Language and Automata Theory and Applications, LATA 2010, volume 6031 of Lecture Notes in Computer Science, pages 118-129. Springer, 2010. (c) Springer.
[ pdf ]

We consider the inclusion and equivalence problem for unambiguous Büchi automata. We show that for a strong version of unambiguity introduced by Carton and Michel these two problems are solvable in polynomial time. We generalize this to Büchi automata with a fixed finite degree of ambiguity in the strong sense. We also discuss the problems that arise when considering the decision problems for the standard notion of ambiguity for Büchi automata.

[CLNW10] A. Carayol, C. Löding, D. Niwinski, and I. Walukiewicz. Choice functions and well-orderings over the infinite binary tree. Central European Journal of Mathematics, 8(4):662-682, 2010. Extended version of [CL07a].
[ pdf ]

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 show how the result can be used to prove the inherent ambiguity of languages of infinite trees. 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.

[CHL10] K. Chatterjee, F. Horn, and C. Löding. Obliging games. In 21st International Conference on Concurrency Theory, CONCUR 2010, volume 6269 of Lecture Notes in Computer Science, pages 284-296. Springer, 2010.
[ pdf ]

Graph games of infinite length provide a natural model for open reactive systems: one player (Eve) represents the controller and the other player (Adam) represents the environment. The evolution of the system depends on the decisions of both players. The specification for the system is usually given as an omega-regular language L over paths and Eve's goal is to ensure that the play belongs to L irrespective of Adam's behaviour. The classical notion of winning strategies fails to capture several interesting scenarios. For example, strong fairness (Streett) conditions are specified by a number of request-grant pairs and require every pair that is requested infinitely often to be granted infinitely often: Eve might win just by preventing Adam from making any new request, but a ``better'' strategy would allow Adam to make as many requests as possible and still ensure fairness. To address such questions, we introduce the notion of obliging games, where Eve has to ensure a strong condition Phi, while always allowing Adam to satisfy a weak condition Psi. We present a linear time reduction of obliging games with two Muller conditions Phi and Psi to classical Muller games. We consider obliging Streett games and show they are co-NP complete, and show a natural quantitative optimisation problem for obliging Streett games is in FNP. We also show how obliging games can provide new and interesting semantics for multi-player games.

[CL10] T. Colcombet and C. Löding. Regular cost functions over finite trees. In Twenty-Fifth Annual IEEE Symposium on Logic in Computer Science, LICS 2010, pages 70-79. IEEE Computer Society, 2010.
[ pdf ]

We develop the theory of regular cost functions over finite trees: a quantitative extension to the notion of regular languages of trees: Cost functions map each input (tree) to a value in omega+1, and are considered modulo an equivalence relation which forgets about specific values, but preserves boundedness of functions on all subsets of the domain. We introduce nondeterministic and alternating finite tree cost automata for describing cost functions. We show that all these forms of automata are effectively equivalent. We also provide decision procedures for them. Finally, following Büchi's seminal idea, we use cost automata for providing decision procedures for cost monadic logic, a quantitative extension of monadic second order logic.

[FZ10] J. Fearnley and M. Zimmermann. Playing Muller Games in a Hurry. In A. Montanari, M. Napoli, and M. Parente, editors, Proceedings of the First International Symposium on Games, Automata, Logic, and Formal Verification, GandALF 2010, volume 25 of Electronic Proceedings in Theoretical Computer Science, pages 146-161, 2010. Conference version of [FZ12a].
[ pdf | ps ]

This work studies the following question: can plays in a Muller game be stopped after a finite number of moves and a winner be declared. A criterion to do this is sound if Player 0 wins an infinite-duration Muller game if and only if she wins the finite-duration version. A sound criterion is presented that stops a play after at most 3^n moves, where n is the size of the arena. This improves the bound (n!+1)^n obtained by McNaughton and the bound n!+1 derived from a reduction to parity games.

[Fri10] W. Fridman. Formats of Winning Strategies for Six Types of Pushdown Games. In A. Montanari, M. Napoli, and M. Parente, editors, Proceedings of the First Symposium on Games, Automata, Logic, and Formal Verification, GandALF 2010, volume 25. Electronic Proceedings in Theoretical Computer Science, 2010.
[ pdf | ps ]

The solution of parity games over pushdown graphs (Walukiewicz '96) was the first step towards an effective theory of infinite-state games. It was shown that winning strategies for pushdown games can be implemented again as pushdown automata. We continue this study and investigate the connection between game presentations and winning strategies in altogether six cases of game arenas, among them realtime pushdown systems, visibly pushdown systems, and counter systems. In four cases we show by a uniform proof method that we obtain strategies implementable by the same type of pushdown machine as given in the game arena. We prove that for the two remaining cases this correspondence fails. In the conclusion we address the question of an abstract criterion that explains the results.

[FLZ10] W. Fridman, C. Löding, and M. Zimmermann. Degrees of Lookahead in Context-free Infinite Games. Technical Report AIB-2010-20, RWTH Aachen, December 2010.
[ pdf | ps ]

We continue the investigation of delay games, infinite games in which one player may postpone her moves for some time to obtain a lookahead on her opponents moves. We show that the problem of determining the winner of such a game is undecidable for context-free winning conditions. Furthermore, we show that the necessary lookahead to win a context-free delay game cannot be bounded by an elementary function.

[GRT10] James Gross, Frank G. Radmacher, and Wolfgang Thomas. A game-theoretic approach to routing under adversarial conditions. In Proceedings of the 6th IFIP International Conference on Theoretical Computer Science, IFIP TCS 2010, volume 323 of IFIP Advances in Information and Communication Technology, pages 355-370. Springer, 2010. (c) IFIP.
[ pdf ]

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.

[HKT10] Michael Holtmann, Łukasz Kaiser, and Wolfgang Thomas. Degrees of Lookahead in Regular Infinite Games. In Luke Ong, editor, Foundations of Software Science and Computational Structures, volume 6014 of Lecture Notes in Computer Science, pages 252-266. Springer, 2010.

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.

[KRT10] Dominik Klein, Frank G. Radmacher, and Wolfgang Thomas. Moving in a network under random failures: A complexity analysis. Science of Computer Programming, 77(7-8):940-954, 2010. Extended version of [KRT09]. (c) Elsevier.
[ pdf ]

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.

[Nei10] Daniel Neider. Reachability Games on Automatic Graphs. In Proceedings of the 15th International Conference on Implementation and Application of Automata (CIAA 2010), volume 6482 of Lecture Notes in Computer Science, pages 222-230. Springer, 2010.
[ pdf ]

In this work we study two-person reachability games on finite and infinite automatic graphs. For the finite case we empirically show that automatic game encodings are competitive to well-known symbolic techniques such as BDDs, SAT and QBF formulas. For the infinite case we present a novel algorithm utilizing algorithmic learning techniques, which allows to solve huge classes of automatic reachability games.

[NL10] Daniel Neider and Christof Löding. Learning Visibly One-Counter Automata in Polynomial Time. Technical Report AIB-2010-02, RWTH Aachen, January 2010.
[ pdf | ps ]

Visibly one-counter automata are a restricted kind of one-counter automata: The input symbols are typed such that the type determines the instruction that is executed on the counter when the input symbol is read. We present an Angluin-like algorithm for actively learning visibly one-counter automata that runs in polynomial time in characteristic parameters of the target language and in the size of the information provided by the teacher.

[OU10] Jörg Olschewski and Michael Ummels. The complexity of finding reset words in finite automata. In Mathematical Foundations of Computer Science 2010, volume 6281 of Lecture Notes in Computer Science, pages 568-579. Springer, 2010. (c) Springer.
[ pdf ]

We study several problems related to finding reset words in deterministic finite automata. In particular, we establish that the problem of deciding whether a shortest reset word has length k is complete for the complexity class DP. This result answers a question posed by Volkov. For the search problems of finding a shortest reset word and the length of a shortest reset word, we establish membership in the complexity classes FPNP and FPNP[log], respectively. Moreover, we show that both these problems are hard for FPNP[log]. Finally, we observe that computing a reset word of a given length is FNP-complete.

[Sch10] Stefan Schulz. First-Order Logic with Reachability Predicates on Infinite Systems. In Kamal Lodaya and Meena Mahajan, editors, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010), volume 8 of Leibniz International Proceedings in Informatics (LIPIcs), pages 493-504, Dagstuhl, Germany, 2010. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.
[ pdf | http ]

This paper focuses on first-order logic (FO) extended by reachability predicates such that the expressiveness and hence decidability properties lie between FO and monadic second-order logic (MSO): in FO(R) one can demand that a node is reachably from another by some sequence of edges, whereas in FO(Reg) a regular set of allowed edge sequences can be given additionally. We study FO(Reg) logic in infinite grid-like structures which are important in verification. The decidability of logics between FO and MSO on those simple structures turns out to be sensitive to various parameters. Furthermore we introduce a transformation for infinite graphs called setbased unfolding which is based on an idea of Lohrey and Ondrusch. It allows to transfer the decidability of MSO to FO(Reg) onto the class of transformed structures. Finally we extend regular ground tree rewriting with a skeleton tree. We show that graphs specified in this way coincide with those expressible by vertex replacement and product operators. This allows to extend decidability results of Colcombet for FO(R) to those graphs.

[SLW+10] André Stollenwerk, Martin Lang, Marian Walter, Jutta Arens, Rüdger Kopp, and Stefan Kowalewski. Sicherheitskonzept für eine intensivmedizinische Anwendung am Beispiel der ECMO. In Entwurf komplexer Automatisierungssysteme (EKA 2010), volume 11, pages 65-74, May 2010.
[Tho10a] W. Thomas. On monadic theories of monadic predicates. In A. Blass, N. Dershowitz, and W. Reisig, editors, Fields of Logic and Computation, Essays Dedicated to Yuri Gurevich on the Occasion of His 70th Birthday, volume 6300 of Lecture Notes in Computer Science, pages 615-626. Springer, 2010.
[ pdf ]

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 S1 = (N, +1) of the natural numbers and the monadic theory of the binary tree, i.e., of the two-successor structure S2 = ({0, 1}*, · 0, · 1). We consider expansions of these structures by a monadic predicate P. It is known that the monadic theory of (S1, P) is decidable iff the weak monadic theory is, and that for recursive P this theory is in Delta30, i.e. of low degree in the arithmetical hierarchy. We show that there are structures (S2, P) for which the first result fails, and that there is a recursive P such that the monadic theory of (S2, P) is Pi11 -hard.

[Tho10b] W. Thomas. Theoretische Informatik. Informatik Spektrum, 33(5):429-431, 2010. (c) Springer.
[Tho10c] W. Thomas. Theoretische Informatik - ein Kurzprofil. Informatik Spektrum, 33(5):433-437, 2010. (c) Springer.
[ pdf ]
[Tho10d] W. Thomas. When nobody else dreamed of these things - Axel Thue und die Termersetzung. Informatik Spektrum, 33(5):504-508, 2010. (c) Springer.
[ pdf ]
[TW10] W. Thomas and P. Weil. Preface of STACS 2007 Special Issue. Theory Comput. Syst., 46(3):397, 2010.
[Won10] Karianto Wong. Finite automata on unranked trees: Extensions by arithmetical and equality constraints. PhD thesis, RWTH Aachen, 2010.
[ pdf | http ]

The notion of unranked trees has attracted much interest in current research, especially due to their application as formal models of XML documents. In particular, several automata and logic formalisms on unranked trees have been considered (again) in the literature, and many results that had previously been shown for the ranked-tree setting have turned out to hold for the unranked-tree setting as well. In this thesis, we study two kinds of extensions of finite automata on unranked trees, namely, the extension by arithmetical constraints and the extension by subtree-equality constraints. In the first part of the thesis we introduce a framework of automata on unranked trees that unifies two different approaches to incorporating arithmetical constraints known from the literature, namely the global-constraint approach of Klaedtke and Rueß (2003) and the local-constraint approach of Seidl et al. (2003). We investigate the relationship between the two types of arithmetical constraints with respect to language recognition, and we show that the emptiness problem for this automaton model is decidable. In the second part of this thesis, we introduce automata on unranked trees that are equipped with equality and disequality constraints between direct subtrees, thereby extending the corresponding automaton model in the ranked-tree setting, which was introduced by Bogaert and Tison (1982). In the definition of the automaton model, we propose using formulas of monadic second-order logic to capture the possibility of comparing unboundedly many direct subtrees for equality, a feature that arises naturally in light of the unrankedness. Our main result is that the emptiness problem for this automaton model is decidable. Based upon this result, furthermore, we introduce a logic over data words (that is, words over an infinite alphabet) for which the satisfiability problem is decidable.

[Zim10] M. Zimmermann. Parametric LTL Games. Technical Report AIB-2010-11, RWTH Aachen, 2010.
[ pdf | ps ]

We consider graph games of infinite duration with winning conditions in parameterized linear temporal logic, where the temporal operators are equipped with variables for time bounds. In model checking such specifications were introduced as PLTL by Alur et al. and (in a different version called PROMPT-LTL) by Kupferman et al..

Our work lifts their results on model checking for PLTL and PROMPT-LTL to the level of games: we present algorithms that determine whether a player wins a game with respect to some, infinitely many, or all variable valuations. All these algorithms run in doubly-exponential time; so, adding bounded temporal operators does not increase the complexity compared to solving plain LTL games. Furthermore, we show how to determine optimal valuations that allow a player to win a game.

2009

[AMSM+09] S. Albers, A. Marchetti-Spaccamela, Y. Matias, S.E. Nikoletseas, and W. Thomas, editors. Proceedings of the 36th International Colloquium on Automata, Languages and Programming, ICALP 2009, Part I and II, volume 5555 and 5556 of Lecture Notes in Computer Science. Springer, 2009.
[BAT09] K. Bollue, D. Abel, and W. Thomas. Synthesis of behavioral controllers for discrete event systems with NCES-like Petri net models. In Proceedings of the European Control Conference, ECC 2009, 2009.

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.

[FT09] I. Felscher and W. Thomas. Compositionality and reachability with conditions on path lengths. International Journal of Foundations of Computer Science, 20(5):851-868, 2009. (c) World Scientific Publishing Company.
[ pdf | http ]

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.

[HST09a] P. Hänsch, M. Slaats, and W. Thomas. Parametrized Regular Infinite Games and Higher-Order Pushdown Strategies. In FCT 2009, volume 5699 of lncs, pages 181-192. Springer, 2009. A preliminary version is accepted at the conference AutoMathA 2009, Automata: from Mathematics to Applications, Liège, Belgium. (c) Springer.
[ pdf ]

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.

[HST09b] P. Hänsch, M. Slaats, and W. Thomas. Parametrized Regular Infinite Games and Higher-Order Pushdown Strategies. Technical Report AIB-2009-18, RWTH Aachen, sep 2009. Full version of [HST09a].
[ pdf | ps ]

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.

[KRT09] Dominik Klein, Frank G. Radmacher, and Wolfgang Thomas. The complexity of reachability in randomized sabotage games. In Proceedings of the 3rd International Conference on Fundamentals of Software Engineering, FSEN 2009, volume 5961 of Lecture Notes in Computer Science, pages 162-177. Springer, 2009. (c) Springer.
[ pdf ]

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.

[Lan09] M. Lang. Entwicklung eines dezentral implementierten Sicherheitskonzeptes für intensivmedizinische Anwendungen. Bachelor Thesis, RWTH Aachen, 2009.
[ pdf ]

Das Krankheitsbild des akuten Lungenversagens kann sich grundsätzlich aus jeder schweren Allgemeinerkrankung entwickeln. Es zeichnet sich durch eine starke Reduzierung der zur Verfügung stehenden Gasaustauschfläche der Lunge aus. In schweren Fällen dieser Krankheit ist eine ausreichende Sauerstoffversorgung des Patienten auch mit Hilfe von künstlicher Beatmung nicht mehr möglich. Seit Mitte der 70er Jahre wird als ultima ratio Therapie die extrakorporale Membranoxygenierung (ECMO) angewandt. Bei dieser wird das Blut des Patienten in einem extrakorporalen Kreislauf mit Hilfe einer künstlichen Lunge mit Sauerstoff angereichert und von Kohlendioxid befreit. Im Rahmen des SmartECLA-Projekts wird eine optimierte ECMO entwickelt, die eine automatische Regelung der Blutgase und des extrakorporalen Blutflusses vorsieht. Durch spezielle Konzepte zur Verbesserung der Sicherheit soll das hohe Risiko für den Patienten gesenkt werden. Die vorliegende Arbeit analysiert die Risiken, die durch die Nutzung des SmartECLA- Systems für den Patienten entstehen. Dabei wird versucht aus der Informatik bekannte Abstraktionsprinzipien auf die medizinische Anwendungsdomäne zu übertragen. Ausgehend von den erkannten Gefahren werden unter Beachtung der gesetzlichen Rahmenbedingungen und geltender Normen Anforderungen an das System in Form von technischen Sicherheitszielen formuliert, deren Einhaltung einen Betrieb des Systems mit vertretbarem Risiko garantiert. Zur Realisierung dieser Anforderungen werden verschiedene grundlegende Sicherheitsmaßnahmen vorgestellt und evaluiert. Dabei werden insbesondere die durch die DIN EN 60601-1-10 (Festlegungen für physiologische Regelkreise) geforderten Maßnahmen auf ihre Wirksamkeit überprüft. Darüber hinaus wird ein Diagnoseverfahren für die Sauerstoffpartialdruckmessung des Systems vorge- stellt und auf Basis von Messdaten des experimentellen Systems bewertet. Der damit erreichte Grad an Sicherheit wird an den aufgestellten Sicherheitszielen gemessen. Abschließend wird ein Ausblick auf weitere Arbeiten gegeben, die zur vorständigen Umsetzung der Anforderungen nötig sind.

[Löd09] Christof Löding. Logic and automata over infinite trees. Habilitation Thesis, RWTH Aachen, Germany, 2009.
[ pdf ]
[LW09] Christof Löding and Karianto Wong. On nondeterministic unranked tree automata with sibling constraints. In Ravi Kannan and K. Narayan Kumar, editors, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2009), volume 4 of Leibniz International Proceedings in Informatics (LIPIcs), pages 311-322, Dagstuhl, Germany, 2009. Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
[ pdf | http ]

We continue the study of bottom-up unranked tree automata with equality and disequality constraints between direct subtrees. In particular, we show that the emptiness problem for the nondeterministic automata is decidable. In addition, we show that the universality problem, in contrast, is undecidable.

[Sch09] Stefan Schulz. First-Order Logic with Reachability Predicates over Infinite Systems. Diploma thesis, RWTH-Aachen, 2009.
[ pdf ]

The general task in verification is to check whether a given (possibly infinite) system or structure satisfies a given specification. The specification is usually expressed by a logical formula in a fundamental logic like first-order (FO) predicate logic or monadic second-order (MSO) logic. A weakness of FO logic is that reachability properties, which are important in verification, are not definable. To overcome this problem, one can switch to the more powerful MSO logic or use some logic in between like the extension of FO logic by reachability predicates. The latter solution is better since FO logic with reachability tends to be decidable in more structures than MSO logic. In this thesis we present a method to generate infinite structures on which such extensions of FO logic are decidable. The technique is similar to unfolding and transforms a structure by preserving the decidability of logical theories. This allows to transfer known decidability results of MSO logic to FO logic with reachability predicates on the class of transformed structures. In the course of this work we focus on the class of structures of infinite grids which is very important in verification due to its simplicity and the expressiveness of logical formulas in it. The interesting thing is that the decidability of logics between FO and MSO over those simple structures turns out to be very sensitive to various parameters like the number of dimensions, the available relations and the power of reachability in the considered logics. The final investigation of this thesis is concerned with generalizing an equivalence result of a structure class where FO logic with reachability is known to be decidable. The structures of that class can either be described by regular ground term rewriting (RGTR) or by an finite equation system with graph operations. Motivated by results for an extension of the latter formalism we give a generalization of RGTR such that both formalism again represent the same class of structures.

[Tho09c] W. Thomas. The reachability problem over infinite graphs. In A E. Frid, A. Morozov, A. Rybalchenko, and K. W. Wagner, editors, Proceedings of the 4th International Computer Science Symposium in Russia, CSR 2009, volume 5675 of Lecture Notes in Computer Science, pages 12-18. Springer, 2009. (c) Springer.
[ pdf ]

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.

[Tho09b] W. Thomas. Path logics with synchronization. In K. Lodaya, M. Mukund, and R. Ramanujam, editors, Perspectives in Concurrency Theory, IARCS-Universities, pages 469-481. Universities Press, 2009.
[ pdf ]

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.

[Tho09a] W. Thomas. Facets of synthesis: Revisiting Church's problem. In Proceedings of the 12th International Conference on Foundations of Software Science and Computational Structures, FOSSACS 2009, volume 5504 of Lecture Notes in Computer Science, pages 1-14. Springer, 2009. (c) Springer.
[ pdf ]

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.

[Zim09a] M. Zimmermann. Time-optimal Winning Strategies for Poset Games. In S. Maneth, editor, Proceedings of the 14th International Conference on Implementation and Application of Automata, CIAA 2009, volume 5642 of Lecture Notes in Computer Science, pages 217-226. Springer, 2009. Note: this document slightly differs from the printed version because an error in Corollary 1 has been corrected. (c) Springer.
[ pdf | ps ]

We introduce a novel winning condition for infinite two-player games on graphs which extends the request-response condition and better matches concrete applications in scheduling or project planning. In a poset game, a request has to be responded by multiple events in an ordering over time that is compatible with a given partial ordering of the events. Poset games are zero-sum, but there are plays that are more desirable than others, i.e., those in which the requests are served quickly. We show that optimal strategies (with respect to long term average accumulated waiting times) exist. These strategies are implementable with finite memory and are effectively computable.

[Zim09b] M. Zimmermann. Time-optimal Winning Strategies for Poset Games. Technical Report AIB-2009-13, RWTH Aachen, May 2009. Full version of [Zim09a]. Note: this document slightly differs from the original because an error in Corollary 1 has been corrected.
[ pdf | ps ]

We introduce a novel winning condition for infinite two-player games on graphs which extends the request-response condition and better matches concrete applications in scheduling or project planning. In a poset game, a request has to be responded by multiple events in an ordering over time that is compatible with a given partial ordering of the events. Poset games are zero-sum, but there are plays that are more desirable than others, i.e., those in which the requests are served quickly. We show that optimal strategies (with respect to long term average accumulated waiting times) exist. These strategies are implementable with finite memory and are effectively computable.

[Zim09c] M. Zimmermann. Time-optimal Winning Strategies in Infinite Games. Diplomarbeit, RWTH Aachen, 2009.
[ pdf ]

Infinite Games are an important tool in the synthesis of finite-state controllers for reactive systems. The interaction between the environment and the system is modeled by a finite graph. The specification that has to be satisfied by the controlled system is translated into a winning condition on the infinite paths of the graph. Then, a winning strategy is a controller that is correct with respect to the given specification. Winning strategies are often finitely described by automata with output.

While classical optimization of synthesized controllers focuses on the size of the automaton we consider a different quality measure. Many winning conditions allow a natural definition of waiting times that reflect periods of waiting in the original system. We investigate time-optimal strategies for Request-Response Games, Poset Games - a novel type of infinite games that extends Request-Response Games - and games with winning conditions in Parametric Linear Temporal Logic. Here, the temporal operators of classical Temporal Logics can be subscribed with free variables that represent bounds on the satisfaction. Then, one is interested in winning strategies with respect to optimal valuations of the free variables. The optimization objective, maximization respectively minimization of the variable values, depends on the formula.

For Request-Response Games and Poset Games, we prove the existence of time-optimal finite-state winning strategies. For games with winning conditions in Parametric Linear Temporal Logic, we prove that optimal winning strategies are computable for solitary games.

2008

[Alt08] J. Altenbernd. On bifix systems and generalizations. In Proceedings of the 2nd International Conference on Language and Automata Theory and Applications, LATA 2008, volume 5196 of Lecture Notes in Computer Science, pages 40-51. Springer, 2008. (c) Springer.
[ pdf ]

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.

[CS08] A. Carayol and M. Slaats. Positional Strategies for Higher-Order Pushdown Parity Games. In Mathematical Foundations of Computer Science 2008, volume 5162 of Lecture Notes in Computer Science, pages 217-228. Springer, 2008. (c) Springer.
[ pdf ]

Higher-order pushdown systems generalize pushdown systems by using higher-order stacks, which are nested stacks of stacks. In this article, we consider parity games defined by higher-order pushdown systems and provide a k-Exptime algorithm to compute finite representations of positional winning strategies for both players for games defined by level-k higher-order pushdown automata. Our result is based on automata theoretic techniques exploiting the tree structure corresponding to higher-order stacks and their associated operations.

[CL08b] T. Colcombet and C. Löding. The non-deterministic Mostowski hierarchy and distance-parity automata. In Proceedings of the 35th International Colloquium on Automata, Languages and Programming, ICALP 2008, volume 5126 of Lecture Notes in Computer Science, pages 398-409. Springer, 2008. (c) Springer.
[ pdf ]

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.

[CL08a] T. Colcombet and C. Löding. The nesting-depth of disjunctive mu-calculus for tree languages and the limitedness problem. In Proceedings of the 17th EACSL Annual Conference on Computer Science Logic CSL 2008, volume 5213 of Lecture Notes in Computer Science. Springer, 2008. (c) Springer.
[ pdf ]

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.

[Fel08] I. Felscher. The Compositional Method and Regular Reachability. In Proceedings of the 2nd Workshop on Reachability Problems, Liverpool, UK, September 15-17,2008, volume 223 of Electronic Notes in Theoretical Computer Science, pages 103-117. Elsevier Science Publishers, 2008.
[ pdf | http ]

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.

[HTW08] F. Horn, W. Thomas, and N. Wallmeier. Optimal strategy synthesis for request-response games. In Proceedings of the 6th International Symposium on Automated Technology for Verification and Analysis, ATVA 2008, volume 5311 of Lecture Notes in Computer Science, pages 361-373. Springer, 2008. (c) Springer.
[ pdf ]

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.

[Nei08] Daniel Neider. Lernverfahren für Automaten über linearisierten XML-Dokumenten. In Informatik Spektrum. Springer, 2008. (c) Springer.
[ pdf ]

Wir untersuchen die Validierung von XML-Dokumenten gegen DTDs mittels endlicher Automaten. Da für die Konstruktion solcher endlicher Automaten noch keine allgemeine Konstruktionsmethode bekannt ist, präsentieren wir einen auf Lernverfahren basierenden Ansatz. In diesem Zusammenhang entwickeln wir ein polynomielles Lernverfahren für visibly 1-Zählerautomaten mit beliebigem Schwellenwert.

[Rad08a] Frank G. Radmacher. An automata theoretic approach to rational tree relations. In Proceedings of the 34th International Conference on Current Trends in Theory and Practice of Computer Science, SOFSEM 2008, volume 4910 of Lecture Notes in Computer Science, pages 424-435. Springer, 2008. (c) Springer.
[ pdf ]

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.

[Rad08b] Frank G. Radmacher. An automata theoretic approach to the theory of rational tree relations. Technical Report AIB-2008-05, RWTH Aachen, March 2008. Full version of [Rad08a].
[ pdf | ps ]

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.

[Tho08c] W. Thomas. Optimizing winning strategies in regular infinite games. In Proceedings of the 34th Conference on Current Trends in Theory and Practice of Computer Science, SOFSEM 2008, volume 4910 of Lecture Notes in Computer Science, pages 118-123. Springer, 2008. (c) Springer.
[ pdf ]

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

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

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

[Tho08d] W. Thomas. Solution of Church's problem: A tutorial. In K. Apt and R. van Rooij, editors, New Perspectives on Games and interaction, volume 4. Amsterdam University Press, 2008.
[ pdf ]

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.

[Tho08b] W. Thomas. Model transformations in decidability proofs for monadic theories. In M. Kaminski and S. Martini, editors, Proceedings of the 17th EACSL Annual Conference on Computer Science Logic, CLS 2008, volume 5213 of Lecture Notes in Computer Science, pages 23-31. Springer, 2008. (c) Springer.
[ pdf ]

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.

[Wal08] Nico Wallmeier. Strategien in unendlichen Spielen mit Liveness-Gewinnbedingungen : Syntheseverfahren, Optimierung und Implementierung. PhD thesis, RWTH Aachen, 2008.
[ pdf | http ]

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.

2007

[BCL07] A. Blumensath, T. Colcombet, and C. Löding. Logical theories and compatible operations. In J. Flum, E. Grädel, and T. Wilke, editors, Logic and automata: History and Perspectives, pages 72-106. Amsterdam University Press, 2007. Note: This version slightly differs from the printed version because an error in Theorem 3.19 has been corrected.
[ pdf ]
[CL07a] Arnaud Carayol and Christof Löding. MSO on the infinite binary tree: Choice and order. In Proceedings of the 16th Annual Conference of the European Association for Computer Science Logic, CSL 2007, volume 4646 of Lecture Notes in Computer Science, pages 161-176. Springer, 2007. (c) Springer.
[ pdf ]

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.

[CL07b] T. Colcombet and C. Löding. Transforming structures by set interpretations. Logical Methods in Computer Science, 3(2), 2007.
[ pdf ]

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.

[EFT07] H.-D. Ebbinghaus, J. Flum, and W. Thomas. Einführung in die mathematische Logik. Spektrum Akademischer Verlag, Heidelberg, fifth edition, 2007.
[Hol07] M. Holtmann. Memory Reduction for Strategies in Infinite Games. Diploma Thesis (revised version), RWTH Aachen, 2007.
[ pdf | ps ]

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.

[HL07] Michael Holtmann and Christof Löding. Memory Reduction for Strategies in Infinite Games. In Jan Holub and Jan Zdárek, editors, Implementation and Application of Automata, 12th International Conference, CIAA 2007, Prague, Czech Republic, July 16-18, 2007, Revised Selected Papers, volume 4783 of Lecture Notes in Computer Science, pages 253-264. Springer, 2007.
[ pdf | ps ]

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.

[KL07] Wong Karianto and Christof Löding. Unranked tree automata with sibling equalities and disequalities. In Proceedings of the 34th International Colloquium on Automata, Languages and Programming, ICALP 2007, volume 4596 of Lecture Notes in Computer Science, pages 875-887. Springer, 2007. (c) Springer.
[ pdf ]

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.

[LLS07] Christof Löding, Carsten Lutz, and Olivier Serre. Propositional dynamic logic with recursive programs. Journal of Logic and Algebraic Programming, 73:51-69, 2007. Full version of [LS06].
[ pdf ]

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.

[LS07] Christof Löding and Alex Spelten. Transition Graphs of Rewriting Systems over Unranked Trees. In Proceedings of the 32nd International Symposium on Mathematical Foundations of Computer Science, MFCS 2007, volume 4708 of Lecture Notes in Computer Science, pages 67-77. Springer, 2007. Full version (with appendix). A preliminary version is accepted at the international conference AutoMathA 2007, Automata: from Mathematics to Applications, Palermo, Italy. (c) Springer.
[ pdf | ps ]

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.

[Nei07] D. Neider. Learning Automata for Streaming XML Documents. Diploma thesis, RWTH Aachen, 2007.
[ pdf | ps ]
[RT07a] A. Rabinovich and W. Thomas. Logical refinements of Church's problem. In Proceedings of the 16th Annual Conference of the European Association for Computer Science Logic, CSL 2007, volume 4646 of Lecture Notes in Computer Science, pages 69-83. Springer, 2007. (c) Springer.
[ pdf | ps ]

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.

[Rad07] Frank G. Radmacher. Automatendefinierbare Relationen über Bäumen. Diploma thesis (revised version), RWTH Aachen, 2007.
[ pdf ]

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.

[RT07b] Frank G. Radmacher and Wolfgang Thomas. A game theoretic approach to the analysis of dynamic networks. In Proceedings of the 1st Workshop on Verification of Adaptive Systems, VerAS 2007, volume 200(2) of Electronic Notes in Theoretical Computer Science, pages 21-37, Kaiserslautern, Germany, 2007. Elsevier Science Publishers. (c) Elsevier.
[ pdf ]

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.

[Sla07] M. Slaats. Infinite games over higher-order pushdown systems. Diplomarbeit, RWTH Aachen, 2007.
[ pdf | ps ]

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.

[TW07] W. Thomas and P. Weil, editors. Proceedings of the 24th Annual Symposium on Theoretical Aspects of Computer Science, STACS 2007, volume 4393 of Lecture Notes in Computer Science. Springer, 2007.
[WT07] Stefan Wöhrle and Wolfgang Thomas. Model checking synchronized products of infinite transition systems. Logical Methods in Computer Science, 3(4), 2007.
[ pdf | ps ]

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.

2006

[BLS06] Vince Bárány, Christof Löding, and Olivier Serre. Regularity problems for visibly pushdown languages. In Proceedings of the 23rd Annual Symposioum on Theoretical Aspects of Computer Science, STACS 2006, volume 3884 of Lecture Notes in Computer Science, pages 420-431. Springer, 2006. (c) Springer.
[ pdf | ps ]

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.

[BKL+06] M. Benedikt, B. Kuijpers, C. Löding, J. Van den Bussche, and Th. Wilke. A characterization of first-order topological properties of planar spatial data. Journal of the ACM, 53(2):273-305, 2006. Full version of [BLVdBW04].
[ pdf ]

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.

[DT06] B. Durand and W. Thomas, editors. Proceedings of the 23rd Annual Symposium on Theoretical Aspects of Computer Science, STACS 2006, volume 3884 of Lecture Notes in Computer Science. Springer, 2006.
[KKT06] Wong Karianto, Aloys Krieg, and Wolfgang Thomas. On intersection problems for polynomially generated sets. In Proceedings of the 33rd International Colloquium on Automata, Languages and Programming, ICALP 2006, Part II, volume 4052 of Lecture Notes in Computer Science, pages 516-527. Springer, 2006. (c) Springer.
[ pdf | ps ]

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.

[KL06] Wong Karianto and Christof Löding. Unranked tree automata with sibling equalities and disequalities. Technical Report AIB-2006-13, RWTH Aachen, October 2006.
[ pdf | ps ]

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.

[Löd06] Christof Löding. Reachability problems on regular ground tree rewriting graphs. Theory of Computing Systems, 39(2):347-383, 2006.
[ pdf ]

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.

[LS06] Christof Löding and Olivier Serre. Propositional dynamic logic with recursive programs. volume 3921 of Lecture Notes in Computer Science, pages 292-306. Springer, 2006. (c) Springer.
[ pdf ]

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.

[RT06] A. Rabinovich and W. Thomas. Decidable theories of the ordering of natural numbers with unary predicates. In Proceedings of the 15th Annual Conference of the European Association for Computer Science Logic, CSL 2006, volume 4207 of Lecture Notes in Computer Science, pages 562-574. Springer, 2006. (c) Springer.
[ pdf ]

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

[Roh06b] Philipp Rohde. On the mu-calculus augmented with sabotage. In Proceedings of the 9th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2006, volume 3921 of Lecture Notes in Computer Science, pages 142-156. Springer, 2006. (c) Springer.
[ pdf ]

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

[Roh06a] Philipp Rohde. On games and logics over dynamically changing structures. PhD thesis, RWTH Aachen, 2006.
[ pdf ]

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

[SATW06] C. Schulte Althoff, W. Thomas, and N. Wallmeier. Observations on determinization of Büchi automata. Theoretical Computer Science, 363(2):224-233, October 2006.
[ pdf | ps ]

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

[Spe06] A. Spelten. Rewriting Systems over Unranked Trees. Diplomarbeit, RWTH Aachen, 2006.
[ pdf | ps ]

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.

[Tho06] W. Thomas. Automata theory and infinite transition systems. In Preproceedings of EMS Summer School CANT 2006, Prépublication 06.002, Institut de Mathématique, Université de Liège, May 2006, 2006.
[ pdf ]

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.

2005

[CLT05] Julien Cristau, Christof Löding, and Wolfgang Thomas. Deterministic automata on unranked trees. In Proceedings of the 15th International Symposium on Fundamentals of Computation Theory, FCT 2005, Lecture Notes in Computer Science. Springer, 2005. (c) Springer.
[ pdf ]

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.

[Kar05a] Wong Karianto. Adding monotonic counters to automata and transition graphs. In Proceedings of the 9th International Conference on Developments in Language Theory, DLT 2005, volume 3572 of Lecture Notes in Computer Science, pages 308-319. Springer, 2005. (c) Springer.
[ pdf | ps ]

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.

[Kar05b] Wong Karianto. On Parikh images of higher-order pushdown automata. In 15. Theorietag der GI Fachgruppe 0.1.5 Automaten und Formale Sprachen, Technical Report WSI-2005-16, pages 26-29. Wilhelm-Schickard-Institut für Informatik, Eberhard-Karls-Universität Tübingen, 2005.
[ pdf | ps ]

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.

[SATW05] C. Schulte Althoff, W. Thomas, and N. Wallmeier. Observations on determinization of Büchi automata. In Proceedings of the 10th International Conference on the Implementation and Application of Automata, CIAA 2005, volume 3845 of Lecture Notes in Computer Science, pages 262-272. Springer, 2005. (c) Springer.
[ pdf | ps ]

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

[Tho05] W. Thomas. Some perspectives of infinite-state verification. In Proceedings of the 3rd International Symposium on Automated Technology for Verification and Analysis, ATVA 2005, volume 3707 of Lecture Notes in Computer Science, pages 3-10. Springer, 2005. (c) Springer.
[ pdf ]

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.

[Wöh05] S. Wöhrle. Decision problems over infinite graphs: Higher-order pushdown systems and synchronized products. PhD thesis, RWTH Aachen, 2005.
[ pdf | ps ]

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.

2004

[BLVdBW04] M. Benedikt, C. Löding, J. Van den Bussche, and Th. Wilke. A characterization of first-order topological properties of planar spatial data. In Proceedings of the 23rd ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems, PODS 2004, pages 107-114. ACM Press, 2004.
[ pdf ]

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.

[BSL04] Yves Bontemps, Pierre Yves Schobbens, and Christof Löding. Synthesis of open reactive systems from scenario-based specifications. Fundamenta Informaticae, 62(2):139-169, 2004.
[ ps ]

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.

[CL04] Th. Colcombet and C. Löding. On the expressiveness of deterministic transducers over infinite trees. In Proceedings of the 21st Annual Symposioum on Theoretical Aspects of Computer Science, STACS 2004, volume 2996 of Lecture Notes in Computer Science, pages 428-439. Springer, 2004. (c) Springer.
[ pdf | ps ]

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.

[GW04] M. Grohe and S. Wöhrle. An existential locality theorem. Annals of Pure and Applied Logic, 129:131-148, 2004.

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.

[Kar04] Wong Karianto. Parikh automata with pushdown stack. Diplomarbeit, RWTH Aachen, 2004.
[ pdf ]

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.

[KT04] M. Kats and W. Thomas. Metaregular languages: A logical point of view. In Workshop Formale Methoden der Linguistik und 14. Theorietag Automaten und Formale Sprachen. Caputh bei Potsdam, 27. September - 30. September 2004, pages 89-93. Institut für Informatik, Universität Potsdam, 2004.
[ ps ]

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

[LMS04] Christof Löding, P. Madhusudan, and Olivier Serre. Visibly pushdown games. In Proceedings of the 24th Conference on Foundations of Software Technology and Theoretical Computer Science, FST TCS 2004, volume 3328 of Lecture Notes in Computer Science, pages 408-420. Springer, 2004. (c) Springer.
[ pdf ]

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.

[Roh04] Philipp Rohde. Moving in a crumbling network: The balanced case. In Proceedings of the 18th International Workshop on Computer Science Logic, CSL 2004, volume 3210 of Lecture Notes in Computer Science, pages 310-324. Springer, 2004. (c) Springer.
[ pdf | ps ]

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.

[WT04] S. Wöhrle and W. Thomas. Model checking synchronized products of infinite transition systems. In Proceedings of the 19th Annual Symposium on Logic in Computer Science (LICS), pages 2-11. IEEE Computer Society, 2004.
[ pdf | ps ]

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.

2003

[ATW03] J. Altenbernd, W. Thomas, and S. Wöhrle. Tiling systems over infinite pictures and their acceptance conditions. In Proceedings of the 6th International Conference on Developements in Language Theory, DLT 2002, volume 2450 of Lecture Notes in Computer Science, pages 297-306. Springer, 2003. (c) Springer.
[ pdf | ps ]

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.

[Cac03a] T. Cachat. Games on pushdown graphs and extensions. PhD thesis, RWTH Aachen, 2003.
[ pdf | http ]

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.

[Cac03b] T. Cachat. Higher order pushdown automata, the Caucal hierarchy of graphs and parity games. In Proceedings of the 30th International Colloquium on Automata, Languages, and Programming, volume 2719 of Lecture Notes in Computer Science, pages 556-569. Springer, 2003. (c) Springer.
[ pdf | ps ]

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.

[CW03] A. Carayol and S. Wöhrle. The Caucal hierarchy of infinite graphs in terms of logic and higher-order pushdown automata. In Proceedings of the 23rd Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2003, volume 2914 of Lecture Notes in Computer Science, pages 112-123. Springer, 2003. (c) Springer.
[ pdf | ps ]

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.

[GRT03] Eva Giani, Philipp Rohde, and Wolfgang Thomas. A presentation and tutoring environment for courses in theoretical computer science. In Proceedings of the 5th International Conference on New Educational Environments, ICNEE 2003, pages 333-338. net4net, 2003.
[ pdf ]

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.

[Löd03] Christof Löding. Infinite graphs generated by tree rewriting. PhD thesis, RWTH Aachen, Germany, 2003.
[ pdf ]
[LR03b] Christof Löding and Philipp Rohde. Solving the sabotage game is PSPACE-hard. Technical Report AIB-05-2003, RWTH Aachen, 2003.
[ pdf ]

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.

[LR03c] Christof Löding and Philipp Rohde. Solving the sabotage game is PSPACE-hard. In Proceedings of the 28th International Symposium on Mathematical Foundations of Computer Science, MFCS 2003, volume 2747 of Lecture Notes in Computer Science, pages 531-540. Springer, 2003. (c) Springer.
[ pdf | ps ]

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.

[LR03a] Christof Löding and Philipp Rohde. Model checking and satisfiability for sabotage modal logic. In Proceedings of the 23rd Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2003, volume 2914 of Lecture Notes in Computer Science, pages 302-313. Springer, 2003. (c) Springer.
[ pdf | ps ]

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.

[RT03a] Philipp Rohde and Wolfgang Thomas. E-learning in theoretical computer science: Experiences from an undergraduate course. Technical Report AIB-01-2003, Annual Report 2002, Department of Computer Science, Aachen University, 2003.
[ pdf ]
[RT03b] Philipp Rohde and Wolfgang Thomas. Ein e-Lecture-System für die Theoretische Informatik. In Proceedings of the 1st e-Learning Fachtagung Informatik, DeLFI 2003, volume P-37 of Lecture Notes in Informatics, pages 17-26. Gesellschaft für Informatik, 2003.
[ pdf ]

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.

[Tho03a] W. Thomas. Constructing infinite graphs with a decidable MSO-theory. In Proceedings of the 28th International Symposium on Mathematical Foundations of Computer Science, Lecture Notes in Computer Science. Springer, 2003. Corrected version. (c) Springer.
[ ps ]
[Tho03b] W. Thomas. Uniform and nonuniform recognizability. Theoretical Computer Science, 292:299-319, 2003.
[Wal03] N. Wallmeier. Symbolische Synthese zustandsbasierter reaktiver Programme. Diplomarbeit, RWTH Aachen, 2003.
[ pdf | ps ]
[WHT03] N. Wallmeier, P. Hütten, and W. Thomas. Symbolic synthesis of finite-state controllers for request-response specifications. In Proceedings of the 8th International Conference on the Implementation and Application of Automata, CIAA 2003, volume 2759 of Lecture Notes in Computer Science, pages 11-22. Springer, 2003. (c) Springer.
[ pdf | ps ]

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

2002

[Cac02a] T. Cachat. The power of one-letter rational languages. In Proceedings of the 5th international conference Developments in Language Theory, volume 2295 of Lecture Notes in Computer Science, pages 145-154. Springer, 2002. (c) Springer.
[ pdf | ps ]

For any language L, let pow(L)={uj | 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.

[Cac02b] T. Cachat. Symbolic strategy synthesis for games on pushdown graphs. In Proceedings of the 29th International Colloquium on Automata, Languages, and Programming, volume 2380 of Lecture Notes in Computer Science, pages 704-715. Springer, 2002. (c) Springer.
[ pdf | ps ]

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.

[Cac02c] T. Cachat. Two-way tree automata solving pushdown games. In E. Grädel, W. Thomas, and T. Wilke, editors, Automata, Logics, and Infinite Games [GTW02], volume 2500 of Lecture Notes in Computer Science, pages 303-317. Springer, 2002. (c) Springer.
[ pdf | ps ]

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.

[Cac02d] T. Cachat. Uniform solution of parity games on prefix-recognizable graphs. In Antonin Kucera and Richard Mayr, editors, Proceedings of the 4th International Workshop on Verification of Infinite-State Systems, volume 68 of Electronic Notes in Theoretical Computer Science. Elsevier Science Publishers, 2002. (c) Elsevier Science.
[ pdf | ps ]

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.

[CDT02] T. Cachat, J. Duparc, and W. Thomas. Solving pushdown games with a sigma_3 winning condition. In Proceedings of the 11th Annual Conference of the European Association for Computer Science Logic, CSL 2002, volume 2471 of Lecture Notes in Computer Science, pages 322-336. Springer, 2002. (c) Springer.
[ pdf | ps ]

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.

[CT02] O. Carton and W. Thomas. The monadic theory of morphic infinite words and generalizations. Information and Computation, 176:51-76, 2002. Conference version [CT00].
[GTW02] E. Grädel, W. Thomas, and Th. Wilke. Automata, logics, and infinite games, volume 2500 of Lecture Notes in Computer Science. Springer, 2002.
[Löd02a] C. Löding. Ground tree rewriting graphs of bounded tree width. In Proceedings of the 19th International Symposium on Theoretical Aspects of Computer Science, STACS 2002, volume 2285 of Lecture Notes in Computer Science, pages 559-570. Springer, 2002. (c) Springer.
[ ps ]

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.

[Löd02b] C. Löding. Model-checking infinite systems generated by ground tree rewriting. In Proceedings of the 5th International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2002, volume 2303 of Lecture Notes in Computer Science, pages 280-294. Springer, 2002. (c) Springer.
[ ps ]

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.

[LR02] Benedikt Löwe and Philipp Rohde. Games of length omega times two. Proceedings of the American Mathematical Society, 130:1247-1248, 2002.
[ ps ]

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 ω of length ω×2: The determinacy of these games is equivalent to the Axiom of Real Determinacy.

[MST02] O. Matz, N. Schweikardt, and W. Thomas. The monadic quantifier alternation hierachy over grids and graphs. Information and Computation, 179:356-383, 2002.
[Roh02] Philipp Rohde. On the expressive power of the monadic second order logic and the propositional mu-calculus. In E. Grädel, W. Thomas, and T. Wilke, editors, Automata, Logics, and Infinite Games, volume 2500 of Lecture Notes in Computer Science, pages 239-257. Springer, 2002. (c) Springer.
[ ps ]

We consider monadic second order logic (MSO) and the propositional μ-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 ω-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 ω-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.

[Tho02a] W. Thomas. Infinite games and verification. In Proceedings of the International Conference on Computer Aided Verification CAV'02, volume 2404 of Lecture Notes in Computer Science, pages 58-64. Springer, 2002. (c) Springer.
[ ps ]

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.

[Tho02b] W. Thomas. A short introduction to infinite automata. In Proceedings of the 5th international conference Developments in Language Theory, volume 2295 of Lecture Notes in Computer Science, pages 130-144. Springer, 2002. (c) Springer.
[ ps ]

2001

[Cac01] T. Cachat. The power of one-letter rational languages. Technical Report AIB-03-2001, RWTH Aachen, 2001. Preliminary version of [Cac02a].
[ ps ]

For any language L, let pow(L)={uj | 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.

[GW01] M. Grohe and S. Wöhrle. An existential locality theorem. In Proceedings of the 10th Annual Conference of the European Association for Computer Science Logic, CSL 2001, volume 2142 of Lecture Notes in Computer Science, pages 99-114. Springer, 2001. Full version [GW04]. (c) Springer.
[ pdf | ps ]

Gaifman's locality theorem (1981) states that every first-order sentence is equivalent to a Boolean combination of sentences saying: There exist elements a1,...,ak that are far apart from one another, and each ai 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 a1,...,ak that are far apart from one another, and each ai 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.

[Löd01] C. Löding. Efficient minimization of deterministic weak omega-automata. Information Processing Letters, 79(3):105-109, 2001.
[ pdf ]

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.

[Roh01] Philipp Rohde. Über Erweiterungen des Axioms der Determiniertheit. Diplomarbeit, Rheinische Friedrich-Wilhelms-Universität Bonn, 2001.
[ pdf ]

We are considering infinite two-person games with perfect information. The Axiom of Determinacy AD is the following statement: every game of length ω, 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 ω is equivalent to that of all games on integers with length ω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 ADR. The exact boundary in regard to the length of the games is ω*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 ADR.

AD+ is an axiom introduced by Woodin to combine consequences of ADR 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.

[Tho01] W. Thomas. Logic for computer science: The engineering challenge. In R. Wilhelm, editor, Informatics - 10 Years Back. 10 Years Ahead, volume 2000 of Lecture Notes in Computer Science, pages 257-267, Dagstuhl, 2001. Springer. (c) Springer.
[ ps ]
[Wöh01] S. Wöhrle. Lokalität in der Logik und algorithmische Anwendungen. Diplomarbeit, Albert-Ludwigs-Universität Freiburg, 2001.

2000

[CT00] O. Carton and W. Thomas. The monadic theory of morphic infinite words and generalizations. In M. Nielsen and B. Rovan, editors, Proceedings of the 25th International Symposium on Mathematical Foundations of Computer Science, MFCS 2000, volume 1893 of Lecture Notes in Computer Science, pages 275-284, Bratislava, Slovakia, 2000. Springer. Journal version [CT02]. (c) Springer.
[LV00] H. Lescow and J. Vöge. Minimal separating sets for transformations of omega-automata. Theoretical Computer Science, 231:47-58, 2000.
[LT00] C. Löding and W. Thomas. Alternating automata and logics over infinite words. In Proceedings of the IFIP International Conference on Theoretical Computer Science, IFIP TCS2000, volume 1872 of Lecture Notes in Computer Science, pages 521-535. Springer, 2000. (c) Springer.
[ ps ]

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.

[SV00a] D. Schmitz and J. Vöge. Implementation of a strategy improvement algorithm for parity games. In Proceedings of the fifth International conference on Implementation and Application of Automata, pages 45-51, 2000.
[ ps ]
[SV00b] D. Schmitz and J. Vöge. The package omega. Manual, RWTH Aachen, 2000.
[ ps ]
[ST00] M. Steinby and W. Thomas. Trees and term rewriting in 1910: On a paper by Axel Thue. Bulletin of the European Association for Theoretical Computer Science, 72:256-269, 2000.
[ ps ]
[Vög00] J. Vöge. Strategiesynthese für Paritätsspiele auf endlichen Graphen. PhD thesis, RWTH Aachen, 2000.
[ pdf ]
[VJ00a] J. Vöge and M. Jurdzinski. A discrete strategy improvement algorithm for solving parity games. In Proceedings of the 12th International Conference on Computer Aided Verification, CAV, volume 1855 of Lecture Notes in Computer Science, pages 202-215. Springer, 2000. (c) Springer.
[ ps ]
[VJ00b] J. Vöge and M. Jurdzinski. A discrete strategy improvement algorithm for solving parity games. Technical Report AIB-2000-2, RWTH Aachen, 2000.
[ ps ]

1999

[DW99] M. Dickhöfer and Th. Wilke. Timed alternating tree automata: the automata-theoretic solution to the TCTL model checking problem. In Automata, Languages and Programming, 26th international colloquium, volume 1644 of Lecture Notes in Computer Science, pages 281-290. Springer, 1999. (c) Springer.
[Löd99] C. Löding. Optimal bounds for the transformation of omega-automata. In Proceedings of the 19th Conference on Foundations of Software Technology and Theoretical Computer Science, volume 1738 of Lecture Notes in Computer Science, pages 97-109. Springer, 1999. (c) Springer.
[ ps ]

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.

[Mat99] O. Matz. Dot-depth and monadic quantifier elimination over pictures. Technical Report AIB-99-08, RWTH Aachen, 1999.
[ ps ]
[Tho99a] W. Thomas. Boolesche Logik und Büchi-Elgot-Trakhtenbrot-Logik in der Beschreibung diskreter Systeme. In P. Horster, editor, Angewandte Mathematik, insbesondere Informatik, pages 282-300. Vieweg, 1999.
[ ps ]
[Tho99b] W. Thomas. Complementation of Büchi automata revisited. In J. Karhumäki, H.A. Maurer, G. Paun, and G. Rozenberg, editors, Jewels are Forever, Contributions on Theoretical Computer Science in Honor of Arto Salomaa, pages 109-120. Springer, 1999.
[Tho99c] W. Thomas, editor. Proceedings of the 2nd International Conference on Foundations of Software Science and Computation Structures, FoSSaCS '99, volume 1578 of Lecture Notes in Computer Science, Amsterdam, 1999. Springer.
[Wil99b] Th Wilke. CTL+ is exponentially more succinct than CTL. In Foundations of Software Technology and Theoretical Computer Science: 19th Conference, volume 1738 of Lecture Notes in Computer Science, pages 110-121. Springer, 1999. Technical Report: [Wil99c]. (c) Springer.
[Wil99c] Th. Wilke. CTL+ is exponentially more succinct than CTL. Technical Report AIB 99-7, RWTH Aachen, Fachgruppe Informatik, 1999. Conference paper: [Wil99b].
[Wil99a] Th. Wilke. Classifying discrete temporal properties. In STACS'99, volume 1563 of Lecture Notes in Computer Science, pages 32-46. Springer, 1999. (c) Springer.

1998

[DW98] M. Dickhöfer and Th. Wilke. The automata-theoretic method works for TCTL model checking. Technical Report 9811, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität Kiel, 1998.
[LLT98] B. Leoniuk, H. Lescow, and W. Thomas. Singleton acceptance conditions in omega-automata. Technical Report 9808, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel, Germany, 1998.
[Löd98] C. Löding. Methods for the transformation of omega-automata: Complexity and connection to second order logic. Diplomarbeit, Christian-Albrechts-Universität of Kiel, 1998.
[ ps ]
[Mat98c] O. Matz. One quantifier will do in existential monadic second order logic over grids. In Proceedings of the 23rd International Symposium on Mathematical Foundations of Computer Science, volume 1450 of Lecture Notes in Computer Science, pages 751-759. Springer, 1998. (c) Springer.
[ ps ]
[Mat98b] O. Matz. On piecewise testable, starfree, and recognizabel picture languages. In Foundations of Software Science and Computation Structures, volume 1378 of Lecture Notes in Computer Science, pages 203-210. Springer, 1998. (c) Springer.
[ ps ]
[Mat98a] O. Matz. First order closure and the monadic second order alternation hierachy. Technical Report 9807, Christian-Albrechts-Universiät Kiel, 1998.
[ ps ]
[NT98] N. Nielsen and W. Thomas, editors. Computer Science Logic '97, selected papers, volume 1414 of Lecture Notes in Computer Science. Springer, 1998.
[PWW98] D. Peled, Th. Wilke, and P. Wolper. An algorithmic approach for checking closure properties of temporal logic specifications and omega-regular languages. Theoretical Computer Science, 195(2):183-203, 1998.
[TW98] D. Thérien and Th. Wilke. Over words, two variables are as powerful as one quantifier alternation: FO2 = Sigma2 Pi2. In Proceedings of the Thirtieth Annual ACM Symposium on Theory of Computing, pages 234-240, 1998.
[Tho98] W. Thomas. Monadic logic and automata: Recent developments. In Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science, LICS '98, pages 136-138, Indianapolis, Indiana, 1998. IEEE Computer Society.
[Wil98] Th. Wilke. Classifying discrete temporal properties. Habilitationsschrift (post-doctoral thesis), April 1998.

Vor 1998

[BMUV97] N. Buhrke, O. Matz, S. Ulbrand, and J. Vöge. The automata theory package omega. In Proceedings of the 2nd International Workshop on Implementing Automata (WIA), volume 1436 of Lecture Notes in Computer Science, pages 228-231. Springer, 1997. (c) Springer.
[BTV97] N. Buhrke, W. Thomas, and J. Vöge. Ein inkrementeller Ansatz zur effizienten Synthese von Controllern aus Spezifikationen mit temporaler Logik. In Formale Beschreibungstechniken für verteilte Systeme, volume 315 of GMD-Studien, pages 99-108, 1997.
[EVW97] K. Etessami, M.Y. Vardi, and Th. Wilke. First-order logic with two variables and unary temporal logic. In Proceedings 12th Annual IEEE Symposium on Logic in Computer Science, pages 228-235. IEEE, 1997.
[HSW97] J. Hromkovic, S. Seibert, and Th. Wilke. Translating regular expressions into small epsilon-free nondeterministic automata. In STACS'97, volume 1200 of Lecture Notes in Computer Science, pages 55-66. Springer, 1997. (c) Springer.
[LV97] H. Lescow, , and J. Vöge. Minimal seperating sets for Muller automata. In Proceedings of the 2nd International Workshop on Implementing Automata (WIA), volume 1436 of Lecture Notes in Computer Science, pages 109-121. Springer, 1997. (c) Springer.
[Mat97] O. Matz. Regular expressions and context-free grammars for picture languages. In Proceedings of the Symposium on Theoretical Aspects of Computer Science, volume 1200 of Lecture Notes in Computer Science, pages 283-294. Springer, 1997. (c) Springer.
[ ps ]
[MT97] O. Matz and W. Thomas. The monadic quantifier alternation hierachy over graphs is infinite. In Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science, pages 236-244. IEEE, 1997.
[PW97] D. Peled and Th. Wilke. Stutter-invariant temporal properties are expressible without the next-time operator. Information Processing Letters, 63(5):243-246, 1997.
[SW97] S. Seibert and Th. Wilke. Bounds for approximating MAXLINEG3-2 and MAXEkSAT. In Lectures on Proof Verification and Approximation Algorithms, volume 1367 of Lecture Notes in Computer Science, pages 179-212. Springer, 1997. (c) Springer.
[Tho97c] W. Thomas. Elements of an automata theory over partial orders. In D.A. Peled et al., editors, Partial Order Methods in Verification, volume 29 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 25-40. American Mathematical Society, 1997.
[Tho97d] W. Thomas. Languages, automata, and logic. In G. Rozenberg and A. Salomaa, editors, Handbook of Formal Languages, volume III, pages 389-455. Springer, New York, 1997.
[Tho97a] W. Thomas. Automata theory on trees and partial orders. In M. Bidoit and M. Dauchet, editors, Proceedings of the 7th International Joint Conference on Theory and Practice of Software Development, TAPSOFT '97, volume 1214 of Lecture Notes in Computer Science, pages 20-38. Springer, 1997. (c) Springer.
[Tho97b] W. Thomas. Ehrenfeucht games, the composition method, and the monadic theory of ordinal words. In J. Mycielski et al., editors, Structures in Logic and Computer Science, A Selection of Essays in Honor of A. Ehrenfeucht, volume 1261 of Lecture Notes in Computer Science, pages 118-143. Springer, 1997. (c) Springer.
[ pdf ]
[Wil97] Th. Wilke. Star-free picture expressions are strictly weaker than first-order logic. In Automata, Languages and Programming, 24th international colloquium, volume 1256 of Lecture Notes in Computer Science, pages 347-357. Springer, 1997. (c) Springer.
[BLV96] N. Buhrke, H. Lescow, , and J. Vöge. Strategy construction in infinite games with Streett and Rabin chain winning conditions. In Proceeding of the International Conference on Tools and Algorithms for Construction and Analysis of Systems,, volume 1055 of Lecture Notes in Computer Science, pages 207-225. Springer, 1996. (c) Springer.
[EFT96] H.-D. Ebbinghaus, J. Flum, and W. Thomas. Einführung in die Mathematische Logik. Spektrum Akademischer Verlag, Heidelberg, fourth edition, 1996.
[EW96] K. Etessami and Th. Wilke. An until hierarchy for temporal logic. In Proceedings 11th Annual IEEE Symposium on Logic in Computer Science, pages 108-117. IEEE, 1996.
[GRST96] D. Giammarresi, A. Restivo, S. Seibert, and W. Thomas. Monadic second-order logic over rectangular pictures and recognizability by tiling systems. Information and Computation, 125(1):32-45, 1996.
[PWW96] D. Peled, Th. Wilke, and P. Wolper. An algorithmic approach for checking closure properties of omega-regular languages. In Concur '96: Concurrency Theory, volume 1119 of Lecture Notes in Computer Science, pages 596-610. Springer, 1996. (c) Springer.
[ST96] I. Schiering and W. Thomas. Counter-free automata, first-order logic, and star-free expressions extended by prefix oracles. In J. Dassow, G. Rozenberg, and A. Salomaa, editors, Proceedings of the 2nd International Conference on Developments in Language Theory, DLT '95, pages 166-175, Magdeburg, Germany, 1996. World Scientific.
[TW96a] D. Thérien and Th. Wilke. Temporal logic and semidirect products: An effective characterization of the until hierarchy. In Proceedings of the 37th Annual Symposium on Foundations of Computer Science, pages 256-263. IEEE, 1996.
[TW96b] D. Thérien and Th. Wilke. Temporal logic and semidirect products: An effective characterization of the until hierarchy. Technical report 96-28, DIMACS, 1996. Conference paper: [TW96a].
[Tho96] W. Thomas. Languages, automata and logic. Technical Report 9607, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel, Germany, May 1996.
[ ps ]
[Wil96] Th. Wilke. An algebraic characterization of frontier testable tree languages. Theoretical Computer Science, 154(1):85-106, 1996.
[WY96] Th. Wilke and H. Yoo. Computing the Rabin index of a regular language of infinite words. Information and Computation, 130(1):61-70, 1996.
[Mat95] O. Matz. Klassifizierung von Bildsprachen mit rationalen Ausdrücken. Diplomarbeit, Christian-Albrechts-Universität Kiel, 1995.
[MMP+95] O. Matz, A. Miller, A. Potthoff, W. Thomas, and E. Valkema. Report on the programm amore. Technical Report 9507, Christian-Albrechts-Universiät Kiel, 1995.
[MP95] O. Matz and A Potthoff. Computing small nondeterministic finite automata. In Tools and Algorithms for the Construction and analysis of Systems, volume NS-95-s of BRICS Notes Series, pages 74-88, 1995.
[ ps ]
[STT95b] H. Straubing, D. Thérien, and W. Thomas. Regular languages defined with generalized quantifiers. Information and Computation, 118:289-301, 1995.
[STT95a] H. Straubing, D. Thérien, and W. Thomas. Logics for regular languages, finite monoids, and circuit complexity. In J.B. Fountain, editor, Proceedings of the NATO Advanced Seminar on Semigroups, Formal Languages, and Groups, volume 466 of NATO ASI Series C, pages 119-146, York, 1995. Kluwer, Dordrecht.
[Tho95a] W. Thomas. On the synthesis of strategies in infinite games. In E.W. Mayr and C. Puech, editors, Proceedings of the 12th Annual Symposium on Theoretical Aspects of Computer Science, STACS '95, volume 900 of Lecture Notes in Computer Science, pages 1-13. Springer, Berlin, 1995. (c) Springer.
[ ps ]
[Tho95b] W. Thomas. Theoretical Computer Science - Some Subjective Impressions, Talk at ASMICS-Workshop, Evreux, October 1995. http://www.informatik.uni-kiel.de/~wt/#TCS.
[WY95] Th. Wilke and H. Yoo. Computing the Wadge degree, the Lifschitz degree, and the Rabin index of a regular language of infinite words in polynomial time. In TAPSOFT '95: Theory and Practive of Software Development, volume 915 of Lecture Notes in Computer Science, pages 288-302. Springer, 1995. (c) Springer.
[EFT94] H.-D. Ebbinghaus, J. Flum, and W. Thomas. Mathematical logic. Springer, New York, second edition, 1994.
[GRST94] D. Giammarresi, A. Restivo, S. Seibert, and W. Thomas. Monadic second-order logic over rectangular pictures and recognizability by tiling systems. In P. Enjalbert, E.W. Mayr, and K.W. Wagner, editors, Proceedings of the 11th Annual Symposium on Theoretical Aspects of Computer Science, STACS '94, volume 775 of Lecture Notes in Computer Science, pages 365-375. Springer, 1994. (c) Springer.
[JPT94] E. Jurvanen, A. Potthoff, and W. Thomas. Deterministic tree languages recognizable by regular frontier check. In G. Rozenberg and A. Salomaa, editors, Proceedings of the 1st International Conference on Developments in Language Theory, DLT '93, pages 3-17, Turku, Finland, 1994. World Scientific.
[PST94] A. Potthoff, S. Seibert, and W. Thomas. Nondeterminism versus determinism of finite automata over directed acyclic graphs. Bulletin of the Belgian Mathematical Society - Simon Stevin, 1(2):285-298, 1994.
[Tho94a] W. Thomas. Finite-state recognizability and logic: From words to graphs. In B. Pehrson and I. Simon, editors, Proceedings of the IFIP 13th World Computer Congress: Technology and Foundations - Information Processing '94, volume 1, pages 499-506, Hamburg, 1994. North-Holland, Amsterdam.
[Tho94b] W. Thomas. Finite-state strategies in regular infinite games. In P.S. Thiagarajan, editor, Proceedings of the 14th Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS '94, volume 880 of Lecture Notes in Computer Science, pages 149-158. Springer, 1994. (c) Springer.
[Tho94c] W. Thomas. Theoretische Grundlagen der Informatik. Drei Vorträge zur Lehrerfortbildung. Technical report, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel, Germany, 1994.
[TL94] W. Thomas and H. Lescow. Logical specifications of infinite computations. In J.W. de Bakker, W.P. de Roever, and G. Rozenberg, editors, REX School/Symposium 1993: A Decade of Concurrency, volume 803 of Lecture Notes in Computer Science, pages 583-621, Noordwijkerhout, The Netherlands, 1994. Springer. (c) Springer.
[Wil94b] Th. Wilke. Specifying timed state sequences in powerful decidable logics and timed automata. In Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 863 of Lecture Notes in Computer Science, pages 694-715. Springer, 1994. (c) Springer.
[Wil94a] Th. Wilke. Automaten und Logiken zur Beschreibung zeitabhängiger Systeme. Technical Report 9408, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität Kiel, 1994.
[JPT93] E. Jurvanen, A. Potthoff, and W. Thomas. Deterministic tree languages recognizable by regular frontier check. Bericht 9311, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel, Germany, 1993.
[PT93] A. Potthoff and W. Thomas. Regular tree languages without unary symbols are star-free. In Z. Esik, editor, Proceedings of the 9th International Conference on Fundamentals of Computation Theory, FCT '93, volume 710 of Lecture Notes in Computer Science, pages 396-405. Springer, Berlin, 1993. (c) Springer.
[Tho93] W. Thomas. On the Ehrenfeucht-Fraïssé game in theoretical computer science. In M.C. Gaudel and J.P. Jouannaud, editors, Proceedings of the International Joint Conference on Theory and Practice of Software Development, TAPSOFT '93, volume 668 of Lecture Notes in Computer Science, pages 559-568, Orsay, France, 1993. Springer. (c) Springer.
[Wil93a] Th. Wilke. An algebraic theory for regular languages of finite and infinite words. International Journal Algebra and Computation, 3(4):447-489, 1993.
[Wil93d] Th. Wilke. Locally threshold testable languages of infinite words. In STACS'93, volume 665 of Lecture Notes in Computer Science, pages 607-616. Springer, 1993. (c) Springer.
[Wil93b] Th. Wilke. Algebras for classifying regular tree languages and an application to frontier testability. In Automata, Languages and Programming, 20th international colloquium, volume 700 of Lecture Notes in Computer Science, pages 347-358. Springer, 1993. (c) Springer.
[Wil93c] Th. Wilke. Algebras for classifying regular tree languages and an application to frontier testability. Technical Report 9313, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität Kiel, 1993. Conference paper: [Wil93b].
[EFT92] H.-D. Ebbinghaus, J. Flum, and W. Thomas. Einführung in die mathematische Logik. BI Wissenschaftsverlag, Mannheim, third edition, 1992.
[Tho92c] W. Thomas. Infinite trees and automaton definable relations over omega-words. Theoretical Computer Science, 103(1):143-159, 1992.
[Tho92b] W. Thomas. Finite-state recognizability of graph properties. In D. Krob, editor, Théorie des Automates et Applications, volume 176 of Publications de l'Université de Rouen, pages 147-159, 1992.
[Tho92a] W. Thomas. 2. Theorietag ``Automaten und Formale Sprachen'' (proceedings). Report 9220, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel, Germany, 1992.
[Tho92d] W. Thomas. Proceedings of the ASMICS-Workshop ``Logics and Recognizable Sets'', Dersau, October 8-10, 1990. Bericht 9104, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel, Germany, 1992.
[Wil92b] Th. Wilke. Locally threshold testable languages of infinite words. Technical Report 9203, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität Kiel, 1992. Conference paper: [Wil93d].
[Wil92a] Th. Wilke. An algebraic theory for regular languages of finite and infinite words. Technical Report 9202, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität Kiel, 1992. Journal version: [Wil93a].
[Tho91b] W. Thomas. On logics, tilings, and automata. In J. Leach Albert, B. Monien, and M. Rodríguez-Artalejo, editors, Proceedings of the 18th International Colloquium on Automata, Languages and Programming, ICALP '91, volume 510 of Lecture Notes in Computer Science, pages 441-454, Madrid, Spain, 1991. Springer, Berlin. (c) Springer.
[Tho91a] W. Thomas. Neue Aspekte in Rabins Theorie der Baumautomaten. Bericht 9110, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel, Germany, 1991.
[Wil91] Th. Wilke. An Eilenberg Theorem for omega-languages. In Automata, Languages and Programming, 18th international colloquium, volume 510 of Lecture Notes in Computer Science, pages 588-599. Springer, 1991. (c) Springer.
[JPTW90] V. Jansen, A. Potthoff, W. Thomas, and U. Wermuth. A Short Guide to the AMORE System (computing Automata, MOnoids, and Regular Expressions). Technical Report AIB-90-2, RWTH Aachen, 1990.
[Tho90a] W. Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, pages 133-192. Elsevier Science Publishers, Amsterdam, 1990.
[Tho90b] W. Thomas. Infinite trees and automaton definable relations over omega-words. In C. Choffrut and T. Lengauer, editors, Proceedings of the 7th Annual Symposium on Theoretical Aspects of Computer Science, STACS '90, volume 415 of Lecture Notes in Computer Science, pages 263-277, Rouen, France, 1990. Springer. (c) Springer.
[Tho90c] W. Thomas. Logical definability of trace languages. In V. Diekert, editor, Proceedings of the ASMICS-Workshop ``Free Partially Commutative Monoids'', Rep. TUM-I9002, pages 172-182. TU München, 1990.
[KMP+89] V. Kell, A. Maier, A. Potthoff, W. Thomas, and U. Wermuth. AMORE: A system for computing Automata, MOnoids and Regular Expressions. In B. Monien and R. Cori, editors, Proceedings of the 6th Annual Symposium on Theoretical Aspects of Computer Science, STACS '89, volume 349 of Lecture Notes in Computer Science, pages 537-538, Paderborn, Germany, 1989. Springer. (c) Springer.
[Tho89] W. Thomas. Computation tree logic and regular omega-languages. In J.W. de Bakker, W.P. de Roever, and G. Rozenberg, editors, REX Workshop 1988: Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, volume 354 of Lecture Notes in Computer Science, pages 690-713, Noordwijkerhout, The Netherlands, 1989. Springer. (c) Springer.
[STT88] H. Straubing, D. Thérien, and W. Thomas. Regular languages defined with generalized quantifiers. In T. Lepistö and A. Salomaa, editors, Proceedings of the 15th International Colloquium on Automata, Languages and Programming, ICALP '88, volume 317 of Lecture Notes in Computer Science, pages 561-575, Tampere, Finland, 1988. Springer. (c) Springer.
[Tho88] W. Thomas. Automata on infinite objects. Technical Report AIB-88-17, RWTH Aachen, 1988.
[ pdf ]
[HT87] T. Hafer and W. Thomas. Computation tree logic CTL* and path quantifiers in the monadic theory of the binary tree. In T. Ottmann, editor, Proceedings of the 14th International Colloquium on Automata, Languages and Programming, ICALP '87, volume 267 of Lecture Notes in Computer Science, pages 269-279, Karlsruhe, Germany, 1987. Springer. (c) Springer.
[Tho87b] W. Thomas. On chain logic, path logic, and first-order logic over infinite trees. In Proceedings of the 2nd Annual IEEE Symposium on Logic in Computer Science, LICS '87, pages 245-256, Ithaca, N.Y., 1987. IEEE Computer Society Press.
[Tho87a] W. Thomas. A concatenation game and the dot-depth hierarchy. In E. Börger, editor, Computation Theory and Logic, volume 270 of Lecture Notes in Computer Science, pages 415-426. Springer, Berlin, 1987.
[Tho86] W. Thomas. On frontiers of regular trees. RAIRO Theoretical Informatics and Applications, 20:371-381, 1986.
[Tho84a] W. Thomas. An application of the Ehrenfeucht-Fraïssé game in formal language theory. Bull. Soc. Math. France, Mem., 16:11-21, 1984.
[Tho84b] W. Thomas. Logical aspects in the study of tree languages. In B. Courcelle, editor, Proceedings of the 9th International Colloquium on Trees in Algebra and Programming, CAAP '84, pages 31-50. Cambridge University Press, Cambridge, 1984.
[Tho82a] W. Thomas. Classifying regular events in symbolic logic. Journal of Computer and System Sciences, 25(3):360-376, 1982.
[Tho82b] W. Thomas. A hierarchy of sets of infinite trees. In A.B. Cremers and H.P. Kriegel, editors, Proceedings of the 6th GI-Conference on Theoretical Computer Science, volume 145 of Lecture Notes in Computer Science, pages 335-342, Dortmund, Germany, 1982. Springer, Berlin.
[Tho81b] W. Thomas. Remark on the star-height-problem. Theoretical Computer Science, 13:231-237, 1981.
[Tho81a] W. Thomas. A combinatorial approach to the theory of omega-automata. Information and Control, 48(3):261-283, 1981.
[Tho80] W. Thomas. On the bounded monadic theory of well-ordered structures. Journal of Symbolic Logic, 45:334-338, 1980.
[Tho79] W. Thomas. Star-free regular sets of omega-sequences. Information and Control, 42(2):148-156, 1979.