Publications
By Author
Members 
Former Members 
By Year
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 Borellike classification of languages of infinite Mazurkiewicz traces, and provide a solution in the framework of omegaautomata 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 omegaregular trace languages in terms of Muller (word) automata. Finally, we show that the linearization of any omegaregular 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  LeibnizZentrum
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 secondorder 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 coBü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 ``quasiweak'' 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 134145, 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 omegaautomata  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 nonterminating, concurrent behaviors of distributed systems. Here, a corresponding classification is still missing. We introduce the model of ``synchronizationaware 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 omegaregular word languages.

[Cha14a] 
Namit Chaturvedi.
Languages of infinite traces and deterministic asynchronous
automata.
Technical Report AIB201404, 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 omegalanguages 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, synchronizationaware 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 omegaRegular Trace Languages.
arXiv.org, Feb 2014.
CoRR abs/1402.3199. [ pdf  http ]
Mazurkiewicz traces describe concurrent behaviors of distributed systems. Traceclosed 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 omegaregular trace languages in terms of the corresponding traceclosed omegaregular word languages, capturing Erecognizable (reachability) and (deterministically) Büchi recognizable languages. Secondly, we demonstrate the first automatatheoretic result that shows the equivalence of omegaregular traceclosed word languages and Boolean combinations of deterministically Idiamond Büchi recognizable traceclosed languages.

[Fel14] 
Ingo Felscher.
Model composition in modelchecking.
PhD thesis, RWTH Aachen, 2014. [ pdf  http ]
Modelchecking 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 modelchecking (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 firstorder 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 nonelementary lower bound for this size in general for firstorder 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
107113. 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 omegaregular specification without synthesizing a transition system first. His procedure is based on twoway alternating omegaautomata on finite trees that recognize the set of correct programs. We present a more elementary and direct approach using only deterministic bottomup tree automata that compute socalled 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 twoplayer 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 finiteduration 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 1319, 2013. Proceedings, volume
8044 of Lecture Notes in Computer Science, pages 813829. 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 polytime 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 minimallyoverapproximating 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 UrbanaChampaign, 2013. [ pdf ]
We introduce a new paradigm for using blackbox learning to synthesize invariants called ICElearning that learns using examples, counterexamples, and implications, and show that it allows building honest teachers and convergent mechanisms for invariant synthesis. We observe that existing algorithms for blackbox abstract interpretation can be interpreted as monotonic ICE learning algorithms, develop two classes of new nonmonotonic ICElearning 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 nonnegative 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 firstorder 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 wellknown saturation method to annotated prefix replacement systems. Finally, we provide a connection to the study of the logic costWMSO.

[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 327338, Dagstuhl, Germany, 2013. Schloss
DagstuhlLeibnizZentrum 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 PSPACEcomplete 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 PSPACEcomplete.

[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 1631. 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 CEGARlike 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:3045, 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 modelchecking, such specifications were introduced as PLTL by Alur et al. and as PROMPTLTL by Kupferman et al. We show how to determine in doublyexponential 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 triplyexponential running time to determine optimal variable valuations that allow a player to win a game. Finally, we give doublyexponential upper and lower bounds on the values of such optimal variable valuations.

2012
[BLO12] 
Stefan Breuers, Christof Löding, and Jörg Olschewski.
Improved Ramseybased Büchi complementation.
In FoSSaCS 2012, volume 7213 of Lecture Notes in Computer
Science, pages 150164. Springer, 2012.
(c) Springer.
We consider complementing Büchi automata by applying the Ramseybased 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 rankbased complementation. Furthermore, we show how our techniques can be used to improve the Ramseybased complementation such that the asymptotic upper bound for the resulting complement automaton is 2^{O(n log n)} instead of 2^{O(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 171191. 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 contextdependent 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. omegalanguages in regular infinite games.
International Journal of Foundations of Computer Science,
23(05):9851000, 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 omegaword as they choose letters in turn. A game is specified by the omegalanguage which contains the plays won by Player 2. We analyze omegalanguages generated from certain classes K of regular languages of finite words (called *languages), using natural transformations of *languages into omegalanguages. 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:649668, 2012.
Journal version of [FZ10].
International Journal of Foundations of Computer Science (c)
2012 World Scientific Publishing
Company. [ pdf  ps ]
This work considers a finiteduration variant of Muller games, and their connection to infiniteduration Muller games. In particular, it studies the question of how long a finite duration Muller game must be played before the winner of the finiteduration game is guaranteed to be able to win the corresponding infiniteduration game. Previous work by McNaughton has shown that this must occur after Pi_{j=1}^{n}(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 3^{n} moves.

[Fel12] 
I. Felscher.
LTLModelChecking via Model Composition.
In Alain Finkel, Jerome Leroux, and Igor Potapov, editors,
Reachability Problems, 6th International Workshop, RP 2012, Bordeaux, France,
September 1719, 2012. Proceedings, volume 7550 of Lecture Notes in
Computer Science, pages 4253. 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 nonelementary 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 183196, 2012. [ pdf  ps ]
We continue the investigation of finiteduration variants of infiniteduration 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 finiteduration 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 AIB201204, RWTHAachen, 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 431442. Springer Berlin /
Heidelberg, 2012.
10.1007/9783642325892_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 gametheoretic 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 twoplayer 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 nonconnected 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
omegaautomata.
Information Processing Letters, 112(1415):578582, 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 524538.
Springer, 2012. [ pdf ]
A prominent learning algorithm is Angluin's L* algorithm, which allows to learn a minimal deterministic automaton using socalled 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 omegaAutomata 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 764776. Springer Berlin /
Heidelberg, 2012.
10.1007/9783642325892_66. [ pdf  http ]
We show that the regularity and equivalence problems are decidable for deterministic weak pushdown omegaautomata, 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 onecounter 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 354369. 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 169182, 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 finitestate winning strategy for one player. This yields a novel antichainbased 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 twoplayer 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 PSPACEcomplete. 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 higherorder pushdown and the
parametrized setting.
PhD thesis, RWTH Aachen, 2012. [ pdf  http ]
Higherorder pushdown systems extend the idea of pushdown systems by using a ``higherorder 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 higherorder pushdown systems in the context of infinite regular games. In the first part, we present a kExpTime algorithm to compute global positional winning strategies for parity games which are played on the configuration graph of a levelk higherorder pushdown system. To represent those winning strategies in a finite way we use a notion of regularity for sets of higherorder stacks that relies on certain (``symmetric'') operations to build higherorder stacks. The construction of the strategies is based on automata theoretic techniques and uses the fact that the higherorder 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 MSOformula varphi(P) with a parameter PN. This corresponds to a three player game where the ith 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: higherorder pushdown automata and collapsible pushdown automata. In the third part, we study higherorder pushdown systems and higherorder counter systems (where the stack alphabet contains only one symbol), by comparing the language classes accepted by corresponding automata. For example, we show that levelk pushdown languages are level(k+1) counter languages.

[WGLW12] 
E. Weingaertner, R. Glebke, M. Lang, and K. Wehrle.
Building a modular bittorrent model for ns3.
In Proceedings of the 2012 workshop on ns3 (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 ns3 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 BitTorrentbased VideoonDemand systems.

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

2011
[BMOU11] 
Patricia Bouyer, Nicolas Markey, Jörg Olschewski, and Michael Ummels.
Measuring permissiveness in parity games: Meanpayoff parity
games revisited.
In Automated Technology for Verification and Analysis, volume
6996 of Lecture Notes in Computer Science, pages 135149. 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 meanpayoff 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 meanpayoff 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. omegalanguages 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
180191. 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 omegaword as they choose letters in turn. A game is specified by the omegalanguage which contains the plays won by Player 2. We analyze omegalanguages generated from certain classes K of regular languages of finite words (called *languages), using natural transformations of *languages into omegalanguages. 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 AIB201112, RWTH Aachen University, 2011.
Full version of [FT11a]. [ pdf  .ps.gz ]
In modelchecking, 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 nonlocal 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 1316, 2011.
Proceedings, volume 6807 of Lecture Notes of Computer Science, pages
130141, 2011. [ http ]
In modelchecking, 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 nonlocal 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 Contextfree 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
264276, Dagstuhl, Germany, 2011. Schloss DagstuhlLeibnizZentrum 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 contextfree winning conditions. Furthermore, we show that the necessary lookahead to win a deterministic contextfree delay game cannot be bounded by any elementary function. Both results hold already for restricted classes of deterministic contextfree 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 AdrianHoria Dediu, Shunsuke Inenaga, and Carlos MartínVide,
editors, Language and Automata Theory and Applications, volume 6638 of
Lecture Notes in Computer Science, pages 286297. 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 4660. 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 131145,
2011. [ pdf ]
A gametheoretic 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 twoplayer 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 nonconnected 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 twoplayer games constitute a powerful and flexible framework for the design and verification of reactive systems. It is wellknown 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 finitestate 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 finitestate 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.
Resourcebounded 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 Bautomata) 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 nochange. 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 resourcebound 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 resourcecost 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 firstorder 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 306320. Springer, 2011. [ pdf ]
We consider safety games on finite, edgelabeled 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 NPcomplete), 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 AIB201114, 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 InfiniteState Systems, volume 73
of EPTCS, pages 2034, 2011. [ pdf ]
We provide decidability and undecidability results on the modelchecking 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 modelchecking is shown decidable for MSOlogic, we show decidability of the tree modelchecking 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 equallevel 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 MuchnikWalukiewicz.

[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 1921. 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 146161, 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 ]

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 modelchecking), and we determine the connection between the classes of such graphs and other wellstudied 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 contextfree languages, and is itself properly included in the class of contextsensitive 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 modelchecking 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, JoostPieter 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 360364. Springer, 2010. [ pdf ]
This paper presents libalf, a comprehensive, opensource library for learning formal languages. libalf covers various wellknown 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 onecounter automata). libalf is flexible and allows facilely interchanging learning algorithms and combining domainspecific features in a plugandplay 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 DiscreteEvent Systems (WODES'10),
IFAC, pages 3037, 2010. [ pdf ]
In Bollue et al. (2009), a methodology was introduced for the synthesis of behavioral controllers for discreteevent systems. The approach is based on NCESlike 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 118129. 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 wellorderings over the infinite binary
tree.
Central European Journal of Mathematics, 8(4):662682, 2010.
Extended version of [CL07a]. [ pdf ]
We give a new proof showing that it is not possible to define in monadic secondorder 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 nonexistence of an MSOdefinable wellfounded order on the infinite binary tree by showing that every infinite binary tree with a wellfounded order has an undecidable MSOtheory.

[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
284296. 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 omegaregular 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 requestgrant 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 coNP 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 multiplayer games.

[CL10] 
T. Colcombet and C. Löding.
Regular cost functions over finite trees.
In TwentyFifth Annual IEEE Symposium on Logic in Computer
Science, LICS 2010, pages 7079. 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 146161, 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 infiniteduration Muller game if and only if she wins the finiteduration 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 infinitestate 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 Contextfree Infinite Games.
Technical Report AIB201020, 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 contextfree winning conditions. Furthermore, we show that the necessary lookahead to win a contextfree delay game cannot be bounded by an elementary function.

[GRT10] 
James Gross, Frank G. Radmacher, and Wolfgang Thomas.
A gametheoretic 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 355370.
Springer, 2010.
(c) IFIP. [ pdf ]
We present a gametheoretic framework for modeling and solving routing problems in dynamically changing networks. The model covers the aspects of reactivity and nontermination, and it is motivated by qualityofservice provisioning in cognitive radio networks where data transmissions are interfered by primary systems. More precisely, we propose an infinite twoplayer 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 252266. 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 nonregular games where the winning condition is given by a contextfree omegalanguage.

[KRT10] 
Dominik Klein, Frank G. Radmacher, and Wolfgang Thomas.
Moving in a network under random failures: A complexity
analysis.
Science of Computer Programming, 77(78):940954, 2010.
Extended version of [KRT09].
(c) Elsevier. [ pdf ]
We analyze a model of faulttolerant 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 PSPACEcomplete: 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 [pepsilon,p+epsilon], is there a strategy for Runner to reach F (resp. to satisfy phi) with a probability >= p'? This PSPACEcompleteness establishes the same complexity as was known for the nonrandomized sabotage games (by the work of Löding and Rohde), and it sharpens the PSPACEcompleteness 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 nonrandomized 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 222230. Springer, 2010. [ pdf ]
In this work we study twoperson reachability games on finite and infinite automatic graphs. For the finite case we empirically show that automatic game encodings are competitive to wellknown 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 OneCounter Automata in Polynomial Time.
Technical Report AIB201002, RWTH Aachen, January 2010. [ pdf  ps ]
Visibly onecounter automata are a restricted kind of onecounter 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 Angluinlike algorithm for actively learning visibly onecounter 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 568579. 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 FP^{NP} and FP^{NP[log]}, respectively. Moreover, we show that both these problems are hard for FP^{NP[log]}. Finally, we observe that computing a reset word of a given length is FNPcomplete.

[Sch10] 
Stefan Schulz.
FirstOrder 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 493504, Dagstuhl, Germany, 2010. Schloss
DagstuhlLeibnizZentrum fuer Informatik. [ pdf  http ]
This paper focuses on firstorder logic (FO) extended by reachability predicates such that the expressiveness and hence decidability properties lie between FO and monadic secondorder 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 gridlike 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 6574, 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 615626. Springer, 2010. [ pdf ]
Pioneers of logic, among them J.R. Büchi, M.O. Rabin, S. Shelah, and Y. Gurevich, have shown that monadic secondorder logic offers a rich landscape of interesting decidable theories. Prominent examples are the monadic theory of the successor structure S_{1} = (N, +1) of the natural numbers and the monadic theory of the binary tree, i.e., of the twosuccessor structure S_{2} = ({0, 1}^{*}, · 0, · 1). We consider expansions of these structures by a monadic predicate P. It is known that the monadic theory of (S_{1}, P) is decidable iff the weak monadic theory is, and that for recursive P this theory is in Delta_{3}^{0}, i.e. of low degree in the arithmetical hierarchy. We show that there are structures (S_{2}, P) for which the first result fails, and that there is a recursive P such that the monadic theory of (S_{2}, P) is Pi_{1}^{1} hard.

[Tho10b] 
W. Thomas.
Theoretische Informatik.
Informatik Spektrum, 33(5):429431, 2010.
(c) Springer. 
[Tho10c] 
W. Thomas.
Theoretische Informatik  ein Kurzprofil.
Informatik Spektrum, 33(5):433437, 2010.
(c) Springer. [ pdf ] 
[Tho10d] 
W. Thomas.
When nobody else dreamed of these things  Axel Thue und
die Termersetzung.
Informatik Spektrum, 33(5):504508, 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 rankedtree setting have turned out to hold for the unrankedtree 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 subtreeequality 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 globalconstraint approach of Klaedtke and Rueß (2003) and the localconstraint 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 rankedtree setting, which was introduced by Bogaert and Tison (1982). In the definition of the automaton model, we propose using formulas of monadic secondorder 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 AIB201011, RWTH Aachen, 2010. [ pdf  ps ]

2009
[AMSM^{+}09] 
S. Albers, A. MarchettiSpaccamela, 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 NCESlike 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):851868, 2009.
(c) World Scientific Publishing Company. [ pdf  http ]
In modelchecking 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 firstorder 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 HigherOrder
Pushdown Strategies.
In FCT 2009, volume 5699 of lncs, pages 181192.
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 omegalanguage parametrized by P. In this context, an omegaword, 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 kth level of the hierarchy, we provide an effective determinacy result and show that winning strategies can be implemented by deterministic levelk pushdown automata.

[HST09b] 
P. Hänsch, M. Slaats, and W. Thomas.
Parametrized Regular Infinite Games and HigherOrder
Pushdown Strategies.
Technical Report AIB200918, 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 omegalanguage parametrized by P. In this context, an omegaword, 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 kth level of the hierarchy, we provide an effective determinacy result and show that winning strategies can be implemented by deterministic levelk 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 162177. Springer, 2009.
(c) Springer. [ pdf ]
We analyze a model of faulttolerant 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 PSPACEcompleteness 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 PSPACEcomplete: Given a game graph with u and F and a probability p' in the interval [pepsilon,p+epsilon], is there a strategy for Runner to reach F with probability >= p'? Our result extends the PSPACEcompleteness 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 SmartECLAProjekts 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 60601110 (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 311322, Dagstuhl, Germany, 2009. Schloss
Dagstuhl  LeibnizZentrum für Informatik. [ pdf  http ]
We continue the study of bottomup 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.
FirstOrder Logic with Reachability Predicates over Infinite
Systems.
Diploma thesis, RWTHAachen, 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 firstorder (FO) predicate logic or monadic secondorder (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 1218. 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 infinitestate 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, IARCSUniversities, pages 469481. Universities
Press, 2009. [ pdf ]
Over trees and partial orders, chain logic and path logic are systems of monadic secondorder logic in which secondorder 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 twodimensional grid for which the finitepath 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 114.
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.
Timeoptimal 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 217226. 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 twoplayer games on graphs which extends the requestresponse 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 zerosum, 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.
Timeoptimal Winning Strategies for Poset Games.
Technical Report AIB200913, 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 twoplayer games on graphs which extends the requestresponse 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 zerosum, 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.
Timeoptimal Winning Strategies in Infinite Games.
Diplomarbeit, RWTH Aachen, 2009. [ pdf ]

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 4051. Springer, 2008.
(c) Springer. [ pdf ]
Motivated by problems in infinitestate 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 HigherOrder Pushdown Parity
Games.
In Mathematical Foundations of Computer Science 2008, volume
5162 of Lecture Notes in Computer Science, pages 217228. Springer,
2008.
(c)
Springer. [ pdf ]
Higherorder pushdown systems generalize pushdown systems by using higherorder stacks, which are nested stacks of stacks. In this article, we consider parity games defined by higherorder pushdown systems and provide a kExptime algorithm to compute finite representations of positional winning strategies for both players for games defined by levelk higherorder pushdown automata. Our result is based on automata theoretic techniques exploiting the tree structure corresponding to higherorder stacks and their associated operations.

[CL08b] 
T. Colcombet and C. Löding.
The nondeterministic Mostowski hierarchy and distanceparity
automata.
In Proceedings of the 35th International Colloquium on Automata,
Languages and Programming, ICALP 2008, volume 5126 of Lecture Notes
in Computer Science, pages 398409. Springer, 2008.
(c) Springer. [ pdf ]
Given a Rabin treelanguage and natural numbers i,j, the language is said to be i,jfeasible if it is accepted by a parity automaton using priorities {i,i+1,...,j}. The i,jfeasibility induces a hierarchy over the Rabintree languages called the Mostowski hierarchy. In this paper we prove that the problem of deciding if a language is i,jfeasible is reducible to the uniform universality problem for distanceparity automata. Distanceparity automata form a new model of automata extending both the nested distance desert automata introduced by Kirsten in his proof of decidability of the starheight problem, and parity automata over infinite trees. Distanceparity 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 nestingdepth of disjunctive mucalculus 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 starheight 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 mucalculus formula with at most k nesting of fixpoints. We show the same result for disjunctive muformulas 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 Kleenestars. The proof, following the approach of Kirsten in the word case, goes by reduction to the decidability of the limitedness problem for nondeterministic 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 1517,2008, volume 223 of Electronic Notes in
Theoretical Computer Science, pages 103117. Elsevier Science Publishers,
2008. [ pdf  http ]
The compositional method, introduced by Feferman and Vaught in 1959, allows to reduce the modelchecking problem for a product structure to the modelchecking problem for its factors. It applies to firstorder 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 (semilinear) 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 requestresponse 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 361373. Springer, 2008.
(c) Springer. [ pdf ]
We show the solvability of an optimization problem on infinite twoplayer games. The winning conditions are of the ``requestresponse'' 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 Qstates and subsequent visits to Pstates. 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 finitestate machine. For the latter claim we use a reduction to the solution of meanpayoff games due to Paterson and Zwick.

[Nei08] 
Daniel Neider.
Lernverfahren für Automaten über linearisierten
XMLDokumenten.
In Informatik Spektrum. Springer, 2008.
(c)
Springer. [ pdf ]
Wir untersuchen die Validierung von XMLDokumenten 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 1Zä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 424435. 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 separaterational 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 AIB200805, 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 separaterational 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 118123. Springer, 2008.
(c) Springer. [ pdf ]
We consider infinite twoplayer games played on finite graphs where the winning condition (say for the first player) is given by a regular omegalanguage. 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 finitestate 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 secondorder 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 finitestate 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 secondorder 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 finitestate 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 2331. Springer, 2008.
(c) Springer. [ pdf ]
We survey two basic techniques for showing that the monadic secondorder 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
LivenessGewinnbedingungen : 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 LivenessEigenschaften fordern. Eine für Anwendungen (etwa in der ControllerSynthese) zentrale LivenessEigenschaft ist die `RequestResponseBedingung'. 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 `StreettBedingungen', in denen für wiederholte Besuche gewisser Zustände wiederholte Besuche anderer Zustände gefordert werden. Es werden verschiedene Lösungsverfahren für RequestResponseSpiele und StreettSpiele vorgestellt, mit Anwendungen etwa in der Analyse von LiveSequenceCharts. Der Hauptbeitrag besteht in einer quantitativen Analyse der RequestResponseSpiele. 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 RequestResponseSpielen (ü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 MeanPayoffSpiele ü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 OmegaAutomaten und zur Lösung unendlicher Spiele.

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 72106. 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 161176. Springer, 2007.
(c) Springer. [ pdf ]
We give a new proof showing that it is not possible to define in monadic secondorder 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 nonexistence of an MSOdefinable wellfounded order on the infinite binary tree by showing that every infinite binary tree with a wellfounded order has an undecidable MSOtheory.

[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 secondorder (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 firstorder 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 treeautomatic 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 omegaautomata. We apply our algorithm to RequestResponse and StaigerWagner 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 1618, 2007, Revised Selected Papers, volume 4783 of
Lecture Notes in Computer Science, pages 253264. 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 RequestResponse and StaigerWagner 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 875887. 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 MSOformulas 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:5169, 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 nonregular programs. Our decision procedure establishes a 2ExpTime upper complexity bound, and we prove a matching lower bound that applies already to rather weak extensions of PDL with nonregular 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 6777. 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 firstorder 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 6983. 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 finitestate 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 wellknown 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 socalled separaterational 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 separateasynchronous tree automata, which recognize exactly the classes of rational and separaterational 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.

[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 2137, 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 modelchecking, 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 modelchecking problems.

[Sla07] 
M. Slaats.
Infinite games over higherorder 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 higherorder pushdown systems. The higherorder pushdown systems extend the usual pushdown systems by the use of higherorder 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 higherorder 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 higherorder 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), firstorder 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 420431. 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 wellmatched words, meaning that the language can be accepted by a finite automaton if only wellmatched words are considered as input.

[BKL^{+}06] 
M. Benedikt, B. Kuijpers, C. Löding, J. Van den Bussche, and Th. Wilke.
A characterization of firstorder topological properties of
planar spatial data.
Journal of the ACM, 53(2):273305, 2006.
Full version of [BLVdBW04]. [ pdf ]
Planar spatial datasets can be modeled by closed semialgebraic 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 516527. Springer, 2006.
(c)
Springer. [ pdf  ps ]
Some classes of sets of vectors of natural numbers are introduced as generalizations of the semilinear sets, among them the 'simple semipolynomial sets.' Motivated by verification problems that involve arithmetical constraints, we show results on the intersection of such generalized sets with semilinear sets, singling out cases where the nonemptiness of intersection is decidable. Starting from these initial results, we list some problems on solvability of arithmetical constraints beyond the semilinear ones.

[KL06] 
Wong Karianto and Christof Löding.
Unranked tree automata with sibling equalities and
disequalities.
Technical Report AIB200613, 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 MSOformulas 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 bruteforce method.

[Löd06] 
Christof Löding.
Reachability problems on regular ground tree rewriting graphs.
Theory of Computing Systems, 39(2):347383, 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 modelchecking 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
292306. 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 nonregular 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 562574. 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 firstorder and monadic secondorder logic. Building on the modeltheoretic 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 firstorder 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 mucalculus 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 142156.
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 crossmodel modality referring to submodels from which a transition has been removed. We add constructors for forming least and greatest monadic fixedpoints 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 PSPACEcomplete while the more general games without a limited access become EXPTIMEcomplete (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 twoplayer 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 crossmodel 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 modeltheoretic 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 fixedpoints. The resulting logic extends the wellknown ?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 mucalculus'.

[SATW06] 
C. Schulte Althoff, W. Thomas, and N. Wallmeier.
Observations on determinization of Büchi automata.
Theoretical Computer Science, 363(2):224233, October 2006. [ pdf  ps ]
The two determinization procedures of Safra and MullerSchupp 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 ``infinitestate 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 bottomup and topdown deterministic automata on unranked trees. We show that for an appropriate definition of bottomup 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 topdown deterministic automata it is well known that they are less expressive than the nondeterministic 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 topdown deterministic automaton. The standard deterministic topdown 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 308319. Springer, 2005.
(c) Springer. [ pdf  ps ]
We analyze models of infinitestate automata extended by monotonic counting mechanisms, starting from the (finitestate) Parikh automata studied by Klaedtke and Rueß. We show that, for linearbounded 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 prefixrecognizable graphs. For prefixrecognizable graphs, however, we show that the extension by monotonic counters retains the decidability of the reachability problem.

[Kar05b] 
Wong Karianto.
On Parikh images of higherorder pushdown automata.
In 15. Theorietag der GI Fachgruppe 0.1.5 Automaten und
Formale Sprachen, Technical Report WSI200516, pages 2629.
WilhelmSchickardInstitut für Informatik, EberhardKarlsUniversität
Tübingen, 2005. [ pdf  ps ]
We introduce the notion of semipolynomial sets, generalizing the notion of semilinear sets, and show that each semipolynomial set is the Parikh image of level 2 pushdown automata, which represent a special class of higherorder 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 262272. Springer, 2005.
(c) Springer. [ pdf  ps ]
The two determinization procedures of Safra and MullerSchupp for Büchi automata are compared, based on an implementation in a program called OmegaDet.

[Tho05] 
W. Thomas.
Some perspectives of infinitestate 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 310. 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: Higherorder 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 higherorder 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 firstorder topological properties of
planar spatial data.
In Proceedings of the 23rd ACM SIGMODSIGACTSIGART Symposium on
Principles of Database Systems, PODS 2004, pages 107114. ACM Press, 2004. [ pdf ]
Closed semialgebraic 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 scenariobased
specifications.
Fundamenta Informaticae, 62(2):139169, 2004. [ ps ]
We propose here Live Sequence Charts with a new, gamebased 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 428439. Springer, 2004.
(c) Springer. [ pdf  ps ]
We introduce topdown deterministic transducers with rational lookahead (transducer for short) working on infinite terms. We show that for such a transducer T', there exists an MSOtransduction T such that for any graph G, unfold(T(G))=T'(unfold(G)). Reciprocally, we show that if an MSOtransduction 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 MSOtransductions 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:131148, 2004.
We prove an existential version of Gaifman's locality theorem and show how it can be applied algorithmically to evaluate existential firstorder 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 contextsensitive. For the latter, we investigate the Parikh images of 2PDArecognizable languages. We extend the framework of semilinear sets to the socalled semipolynomial sets and show that 2PDA's can generate all these sets. However, we also show that there are 2PDArecognizable languages whose Parikh images are not semipolynomial. For the issue of using semipolynomial sets as the constraint sets of Parikh automata, we investigate the emptiness problem for the intersection of a semilinear set and a semipolynomial set. We show two partial results: first, weakening the framework of semilinear sets leads to decidability, and second, strengthening the framework of semipolynomial 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 8993. 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 TimeVariant Automata (TVA) in the sense of Agasandyan [1] and Salomaa [6]. We set up a correspondence (in the style of BüchiElgotTrakhtenbrot'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 408420. Springer, 2004.
(c) Springer. [ pdf ]
The class of visibly pushdown languages has been recently defined as a subclass of contextfree 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 2EXPTIMEcomplete. We also show that pushdown games against LTL specifications and CARET specifications are 3EXPTIMEcomplete. 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 310324. 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 SMLmodels 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 211. IEEE Computer Society, 2004. [ pdf  ps ]
Formal verification using the modelchecking 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), firstorder logic extended by reachability predicates, of the product system can be reduced to the decidability of FO(R) of the components in a FefermanVaught 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 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.

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 297306. Springer, 2003.
(c) Springer. [ pdf  ps ]
Languages of infinite twodimensional words (infinite omegapictures) are studied in the automata theoretic setting of tiling systems. We show that a hierarchy of acceptance conditions as known from the theory of omegalanguages 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 omegalanguages) 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_3condition. 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 556569. Springer, 2003.
(c) Springer. [ pdf  ps ]
We consider twoplayer parity games played on transition graphs of higher order pushdown automata. They are ``gameequivalent'' to a kind of modelchecking 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
higherorder 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 112123. 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 secondorder (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 languagetheoretic operation of a rational mapping by an MSOtransduction and the unfolding by the treegraph operation. The second characterization is noniterative. We show that the family of graphs of the Caucal hierarchy coincides with the family of graphs obtained as the epsilonclosure of configuration graphs of higherorder pushdown automata. While the different characterizations of the graph family show their robustness and thus also their importance, the characterization in terms of higherorder 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 333338. net4net, 2003. [ pdf ]
We report on the development of electures 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 electures and tutorial units in this field of study. Two components are essential: an integrated and contextindependent 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 PSPACEhard.
Technical Report AIB052003, 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 multigraph 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 PSPACEhard 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 PSPACEcomplete.

[LR03c] 
Christof Löding and Philipp Rohde.
Solving the sabotage game is PSPACEhard.
In Proceedings of the 28th International Symposium on
Mathematical Foundations of Computer Science, MFCS 2003, volume 2747 of
Lecture Notes in Computer Science, pages 531540. 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 multigraph 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 PSPACEhardness 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 PSPACEcomplete.

[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 302313. 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 ÃÂtransitiondeletingÃÂ modality and hence a modal logic over changing models. It was shown that the problem of uniform model checking for this logic is PSPACEcomplete. 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 modeltheoretic 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.
Elearning in theoretical computer science: Experiences from an
undergraduate course.
Technical Report AIB012003, Annual Report 2002, Department of
Computer Science, Aachen University, 2003. [ pdf ] 
[RT03b] 
Philipp Rohde and Wolfgang Thomas.
Ein eLectureSystem für die Theoretische
Informatik.
In Proceedings of the 1st eLearning Fachtagung Informatik,
DeLFI 2003, volume P37 of Lecture Notes in Informatics, pages 1726.
Gesellschaft für Informatik, 2003. [ pdf ]
Es wird ein eLectureSystem 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 MSOtheory.
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:299319, 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 finitestate controllers for
requestresponse 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 1122. 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 finitestate controllers. A liftcontroller problem serves as an example for which the implementation of our algorithm has been tested. The specifications consist of safety conditions and socalled ``requestresponseconditions'' (which have the form ``after visiting a state of P later a state of R is visited''). Many reallife problems can be modeled in this framework. We sketch the theoretical solution which synthesizes a finitestate 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 oneletter rational languages.
In Proceedings of the 5th international conference Developments
in Language Theory, volume 2295 of Lecture Notes in Computer Science,
pages 145154. Springer, 2002.
(c) Springer. [ pdf  ps ]
For any language L, let pow(L)={u^{j}  j>= 0, uin L} be the set of powers of elements of L. Given a rational language L (over a finite alphabet), we study the question, posed in [Cal 96], whether pow(L) is rational or not. While leaving open the problem in general, we provide an algorithmic solution for the case of oneletter 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 704715. Springer, 2002.
(c) Springer. [ pdf  ps ]
We consider infinite twoplayer 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.
Twoway 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 303317. 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 Wtree, where W is a finite set of directions, and to use the expressive power of alternating twoway tree automata to answer these questions. Finally it is necessary to translate the 2way tree automaton into an equivalent nondeterministic oneway tree automaton.

[Cac02d] 
T. Cachat.
Uniform solution of parity games on prefixrecognizable graphs.
In Antonin Kucera and Richard Mayr, editors, Proceedings of the
4th International Workshop on Verification of InfiniteState 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 prefixrecognizable 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 322336. Springer, 2002.
(c) Springer. [ pdf  ps ]
We study infinite twoplayer 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_3set in the Borel hierarchy, thus transcending the Boolean closure of Sigma_2sets which arises with the standard automata theoretic winning conditions (such as the Muller, Rabin, or parity condition). We also show that this Sigma_3game 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:5176, 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 559570. 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.
Modelchecking 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 280294.
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 modelchecking 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:12471248, 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 $\omega $ of length $\omega \xc3\x83\xc2\x972$: 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:356383, 2002. 
[Roh02] 
Philipp Rohde.
On the expressive power of the monadic second order logic and
the propositional mucalculus.
In E. Grädel, W. Thomas, and T. Wilke, editors, Automata,
Logics, and Infinite Games, volume 2500 of Lecture Notes in Computer
Science, pages 239257. Springer, 2002.
(c) Springer. [ ps ]

[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 5864. 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 130144. Springer, 2002.
(c) Springer. [ ps ] 
2001
[Cac01] 
T. Cachat.
The power of oneletter rational languages.
Technical Report AIB032001, RWTH Aachen, 2001.
Preliminary version of [Cac02a]. [ ps ]
For any language L, let pow(L)={u^{j}  j >= 0, uin L} be the set of powers of elements of L. Given a rational language L (over a finite alphabet), we study the question, posed in [Cal 96], whether pow(L) is rational or not. While leaving open the problem in general, we provide an algorithmic solution for the case of oneletter 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 99114. Springer, 2001.
Full version [GW04].
(c) Springer. [ pdf  ps ]
Gaifman's locality theorem (1981) states that every firstorder sentence is equivalent to a Boolean combination of sentences saying: There exist elements a_{1},...,a_{k} that are far apart from one another, and each a_{i} satisfies some local condition described by a firstorder formula. We prove that every existential firstorder sentence is equivalent to a positive Boolean combination of sentences saying: There exist elements a_{1},...,a_{k} that are far apart from one another, and each a_{i} satisfies some local condition described by an existential firstorder formula. We then show how a variant of this existential locality theorem can be applied to evaluate existential firstorder 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 omegaautomata.
Information Processing Letters, 79(3):105109, 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 coBü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 FriedrichWilhelmsUniversität Bonn, 2001. [ pdf ]

[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
257267, Dagstuhl, 2001. Springer.
(c) Springer. [ ps ] 
[Wöh01] 
S. Wöhrle.
Lokalität in der Logik und algorithmische Anwendungen.
Diplomarbeit, AlbertLudwigsUniversitä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
275284, Bratislava, Slovakia, 2000. Springer.
Journal version [CT02].
(c) Springer. 
[LV00] 
H. Lescow and J. Vöge.
Minimal separating sets for transformations of omegaautomata.
Theoretical Computer Science, 231:4758, 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 521535. 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 setup: 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 4551, 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:256269, 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 202215. Springer, 2000.
(c) Springer. [ ps ] 
[VJ00b] 
J. Vöge and M. Jurdzinski.
A discrete strategy improvement algorithm for solving parity
games.
Technical Report AIB20002, RWTH Aachen, 2000. [ ps ] 
1999
[DW99] 
M. Dickhöfer and Th. Wilke.
Timed alternating tree automata: the automatatheoretic solution
to the TCTL model checking problem.
In Automata, Languages and Programming, 26th international
colloquium, volume 1644 of Lecture Notes in Computer Science, pages
281290. Springer, 1999.
(c) Springer. 
[Löd99] 
C. Löding.
Optimal bounds for the transformation of omegaautomata.
In Proceedings of the 19th Conference on Foundations of Software
Technology and Theoretical Computer Science, volume 1738 of Lecture
Notes in Computer Science, pages 97109. Springer, 1999.
(c) Springer. [ ps ]
In this paper we settle the complexity of some basic constructions of omegaautomata theory, concerning transformations of automata characterizing the set of omegaregular 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.
Dotdepth and monadic quantifier elimination over pictures.
Technical Report AIB9908, RWTH Aachen, 1999. [ ps ] 
[Tho99a] 
W. Thomas.
Boolesche Logik und BüchiElgotTrakhtenbrotLogik
in der Beschreibung diskreter Systeme.
In P. Horster, editor, Angewandte Mathematik, insbesondere
Informatik, pages 282300. 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 109120. 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 110121. Springer, 1999.
Technical Report: [Wil99c].
(c) Springer. 
[Wil99c] 
Th. Wilke.
CTL^{+} is exponentially more succinct than CTL.
Technical Report AIB 997, 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 3246. Springer, 1999.
(c) Springer. 
1998
[DW98] 
M. Dickhöfer and Th. Wilke.
The automatatheoretic method works for TCTL model checking.
Technical Report 9811, Institut für Informatik und Praktische
Mathematik, ChristianAlbrechtsUniversität Kiel, 1998. 
[LLT98] 
B. Leoniuk, H. Lescow, and W. Thomas.
Singleton acceptance conditions in omegaautomata.
Technical Report 9808, Institut für Informatik und Praktische
Mathematik, ChristianAlbrechtsUniversität zu Kiel, Germany, 1998. 
[Löd98] 
C. Löding.
Methods for the transformation of omegaautomata: Complexity and
connection to second order logic.
Diplomarbeit, ChristianAlbrechtsUniversitä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 751759. 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 203210.
Springer, 1998.
(c) Springer. [ ps ] 
[Mat98a] 
O. Matz.
First order closure and the monadic second order alternation
hierachy.
Technical Report 9807, ChristianAlbrechtsUniversiä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 omegaregular languages.
Theoretical Computer Science, 195(2):183203, 1998. 
[TW98] 
D. Thérien and Th. Wilke.
Over words, two variables are as powerful as one quantifier
alternation: FO^{2} = Sigma_{2} Pi_{2}.
In Proceedings of the Thirtieth Annual ACM Symposium on Theory
of Computing, pages 234240, 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 136138, Indianapolis, Indiana, 1998.
IEEE Computer Society. 
[Wil98] 
Th. Wilke.
Classifying discrete temporal properties.
Habilitationsschrift (postdoctoral thesis), April 1998. 
Prior to 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 228231. 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 GMDStudien, pages 99108, 1997. 
[EVW97] 
K. Etessami, M.Y. Vardi, and Th. Wilke.
Firstorder logic with two variables and unary temporal logic.
In Proceedings 12th Annual IEEE Symposium on Logic in Computer
Science, pages 228235. IEEE, 1997. 
[HSW97] 
J. Hromkovic, S. Seibert, and Th. Wilke.
Translating regular expressions into small epsilonfree
nondeterministic automata.
In STACS'97, volume 1200 of Lecture Notes in Computer
Science, pages 5566. 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 109121. Springer, 1997.
(c) Springer. 
[Mat97] 
O. Matz.
Regular expressions and contextfree grammars for picture
languages.
In Proceedings of the Symposium on Theoretical Aspects of
Computer Science, volume 1200 of Lecture Notes in Computer Science,
pages 283294. 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 236244. IEEE, 1997. 
[PW97] 
D. Peled and Th. Wilke.
Stutterinvariant temporal properties are expressible without
the nexttime operator.
Information Processing Letters, 63(5):243246, 1997. 
[SW97] 
S. Seibert and Th. Wilke.
Bounds for approximating MAXLINEG32 and MAXEkSAT.
In Lectures on Proof Verification and Approximation Algorithms,
volume 1367 of Lecture Notes in Computer Science, pages 179212.
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 2540. 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 389455. 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 2038. 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 118143. Springer,
1997.
(c) Springer. [ pdf ] 
[Wil97] 
Th. Wilke.
Starfree picture expressions are strictly weaker than
firstorder logic.
In Automata, Languages and Programming, 24th international
colloquium, volume 1256 of Lecture Notes in Computer Science, pages
347357. 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 207225. 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 108117. IEEE, 1996. 
[GRST96] 
D. Giammarresi, A. Restivo, S. Seibert, and W. Thomas.
Monadic secondorder logic over rectangular pictures and
recognizability by tiling systems.
Information and Computation, 125(1):3245, 1996. 
[PWW96] 
D. Peled, Th. Wilke, and P. Wolper.
An algorithmic approach for checking closure properties of
omegaregular languages.
In Concur '96: Concurrency Theory, volume 1119 of Lecture
Notes in Computer Science, pages 596610. Springer, 1996.
(c) Springer. 
[ST96] 
I. Schiering and W. Thomas.
Counterfree automata, firstorder logic, and starfree
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 166175, 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 256263. IEEE, 1996. 
[TW96b] 
D. Thérien and Th. Wilke.
Temporal logic and semidirect products: An effective
characterization of the until hierarchy.
Technical report 9628, DIMACS, 1996.
Conference paper: [TW96a]. 
[Tho96] 
W. Thomas.
Languages, automata and logic.
Technical Report 9607, Institut für Informatik und Praktische
Mathematik, ChristianAlbrechtsUniversität zu Kiel, Germany, May 1996. [ ps ] 
[Wil96] 
Th. Wilke.
An algebraic characterization of frontier testable tree
languages.
Theoretical Computer Science, 154(1):85106, 1996. 
[WY96] 
Th. Wilke and H. Yoo.
Computing the Rabin index of a regular language of infinite
words.
Information and Computation, 130(1):6170, 1996. 
[Mat95] 
O. Matz.
Klassifizierung von Bildsprachen mit rationalen
Ausdrücken.
Diplomarbeit, ChristianAlbrechtsUniversität Kiel, 1995. 
[MMP^{+}95] 
O. Matz, A. Miller, A. Potthoff, W. Thomas, and E. Valkema.
Report on the programm amore.
Technical Report 9507, ChristianAlbrechtsUniversiä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 NS95s of BRICS Notes Series, pages 7488, 1995. [ ps ] 
[STT95b] 
H. Straubing, D. Thérien, and W. Thomas.
Regular languages defined with generalized quantifiers.
Information and Computation, 118:289301, 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 119146, 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 113. Springer,
Berlin, 1995.
(c) Springer. [ ps ] 
[Tho95b] 
W. Thomas.
Theoretical Computer Science  Some Subjective
Impressions, Talk at ASMICSWorkshop, Evreux, October 1995.
http://www.informatik.unikiel.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 288302.
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 secondorder 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 365375. 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
317, 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):285298, 1994. 
[Tho94a] 
W. Thomas.
Finitestate 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 499506, Hamburg, 1994. NorthHolland,
Amsterdam. 
[Tho94b] 
W. Thomas.
Finitestate 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
149158. 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, ChristianAlbrechtsUniversitä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 583621, 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 RealTime and FaultTolerant Systems,
volume 863 of Lecture Notes in Computer Science, pages 694715.
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, ChristianAlbrechtsUniversitä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,
ChristianAlbrechtsUniversität zu Kiel, Germany, 1993. 
[PT93] 
A. Potthoff and W. Thomas.
Regular tree languages without unary symbols are starfree.
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 396405. Springer, Berlin,
1993.
(c) Springer. 
[Tho93] 
W. Thomas.
On the EhrenfeuchtFraï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 559568, 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):447489,
1993. 
[Wil93d] 
Th. Wilke.
Locally threshold testable languages of infinite words.
In STACS'93, volume 665 of Lecture Notes in Computer
Science, pages 607616. 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
347358. 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, ChristianAlbrechtsUniversitä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
omegawords.
Theoretical Computer Science, 103(1):143159, 1992. 
[Tho92b] 
W. Thomas.
Finitestate recognizability of graph properties.
In D. Krob, editor, Théorie des Automates et Applications,
volume 176 of Publications de l'Université de Rouen, pages
147159, 1992. 
[Tho92a] 
W. Thomas.
2. Theorietag ``Automaten und Formale Sprachen''
(proceedings).
Report 9220, Institut für Informatik und Praktische Mathematik,
ChristianAlbrechtsUniversität zu Kiel, Germany, 1992. 
[Tho92d] 
W. Thomas.
Proceedings of the ASMICSWorkshop ``Logics and
Recognizable Sets'', Dersau, October 810, 1990.
Bericht 9104, Institut für Informatik und Praktische Mathematik,
ChristianAlbrechtsUniversitä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, ChristianAlbrechtsUniversitä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, ChristianAlbrechtsUniversität Kiel, 1992.
Journal version: [Wil93a]. 
[Tho91b] 
W. Thomas.
On logics, tilings, and automata.
In J. Leach Albert, B. Monien, and M. RodríguezArtalejo,
editors, Proceedings of the 18th International Colloquium on Automata,
Languages and Programming, ICALP '91, volume 510 of Lecture Notes in
Computer Science, pages 441454, 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,
ChristianAlbrechtsUniversität zu Kiel, Germany, 1991. 
[Wil91] 
Th. Wilke.
An Eilenberg Theorem for omegalanguages.
In Automata, Languages and Programming, 18th international
colloquium, volume 510 of Lecture Notes in Computer Science, pages
588599. 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 AIB902, 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 133192. Elsevier
Science Publishers, Amsterdam, 1990. 
[Tho90b] 
W. Thomas.
Infinite trees and automaton definable relations over
omegawords.
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 263277, Rouen,
France, 1990. Springer.
(c) Springer. 
[Tho90c] 
W. Thomas.
Logical definability of trace languages.
In V. Diekert, editor, Proceedings of the ASMICSWorkshop ``Free
Partially Commutative Monoids'', Rep. TUMI9002, pages 172182. 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 537538, Paderborn,
Germany, 1989. Springer.
(c) Springer. 
[Tho89] 
W. Thomas.
Computation tree logic and regular omegalanguages.
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 690713, 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
561575, Tampere, Finland, 1988. Springer.
(c) Springer. 
[Tho88] 
W. Thomas.
Automata on infinite objects.
Technical Report AIB8817, 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 269279, Karlsruhe, Germany,
1987. Springer.
(c) Springer. 
[Tho87b] 
W. Thomas.
On chain logic, path logic, and firstorder logic over infinite
trees.
In Proceedings of the 2nd Annual IEEE Symposium on Logic in
Computer Science, LICS '87, pages 245256, Ithaca, N.Y., 1987. IEEE
Computer Society Press. 
[Tho87a] 
W. Thomas.
A concatenation game and the dotdepth hierarchy.
In E. Börger, editor, Computation Theory and Logic, volume
270 of Lecture Notes in Computer Science, pages 415426. Springer,
Berlin, 1987. 
[Tho86] 
W. Thomas.
On frontiers of regular trees.
RAIRO Theoretical Informatics and Applications, 20:371381,
1986. 
[Tho84a] 
W. Thomas.
An application of the EhrenfeuchtFraïssé game in
formal language theory.
Bull. Soc. Math. France, Mem., 16:1121, 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 3150.
Cambridge University Press, Cambridge, 1984. 
[Tho82a] 
W. Thomas.
Classifying regular events in symbolic logic.
Journal of Computer and System Sciences, 25(3):360376, 1982. 
[Tho82b] 
W. Thomas.
A hierarchy of sets of infinite trees.
In A.B. Cremers and H.P. Kriegel, editors, Proceedings of the
6th GIConference on Theoretical Computer Science, volume 145 of
Lecture Notes in Computer Science, pages 335342, Dortmund, Germany, 1982.
Springer, Berlin. 
[Tho81b] 
W. Thomas.
Remark on the starheightproblem.
Theoretical Computer Science, 13:231237, 1981. 
[Tho81a] 
W. Thomas.
A combinatorial approach to the theory of omegaautomata.
Information and Control, 48(3):261283, 1981. 
[Tho80] 
W. Thomas.
On the bounded monadic theory of wellordered structures.
Journal of Symbolic Logic, 45:334338, 1980. 
[Tho79] 
W. Thomas.
Starfree regular sets of omegasequences.
Information and Control, 42(2):148156, 1979. 