To appear

• Ł. Kaiser. Synthesis for Structure Rewriting Systems. In Proceedings of the 34th International Symposium on Mathematical Foundations of Computer Science, MFCS '09. Springer-Verlag. To appear.                                 
  Abstract   BibTeX

  The description of a single state of a modelled system is often complex in practice, but few procedures for synthesis address this problem in depth. We study systems in which a state is described by an arbitrary finite structure, and changes of the state are represented by structure rewriting rules, a generalisation of term and graph rewriting. Both the environment and the controller are allowed to change the structure in this way, and the question we ask is how a strategy for the controller that ensures a given property can be synthesised. We focus on one particular class of structure rewriting rules, namely on separated structure rewriting, a limited syntactic class of rules. To counter this restrictiveness, we allow the property to be ensured by the controller to be specified in a very expressive logic: a combination of monadic second-order logic evaluated on states and the modal $\mu$-calculus for the temporal evolution of the whole system. We show that for the considered class of rules and this logic, it can be decided whether the controller has a strategy ensuring a given property, and in such case a finite-memory strategy can be synthesised. Additionally, we prove that the same holds if the property is given by a monadic second-order formula to be evaluated on the limit of the evolution of the system.

  @inproceedings{K09,
       author = {Łukasz Kaiser},
       title = {Synthesis for Structure Rewriting Systems},
       booktitle = {Proceedings of the 34th International Symposium on Mathematical Foundations of Computer Science, MFCS '09},
       publisher = {Springer-Verlag},
       note = {To appear},
       url = {http://logic.rwth-aachen.de/~kaiser/graph_games_short.pdf},
  }
  

• M. Ummels and D. Wojtczak. Decision Problems for Nash Equilibria in Stochastic Games. In Proceedings of the 18th Annual Conference of the European Association for Computer Science Logic, CSL '09. Springer-Verlag. To appear.                                 
  Abstract   BibTeX

  We analyse the computational complexity of finding Nash equilibria in stochastic multiplayer games with $\omega$-regular objectives. While the existence of an equilibrium whose payoff falls into a certain interval may be undecidable, we single out several decidable restrictions of the problem. First, restricting the search space to stationary, or pure stationary, equilibria results in problems that are typically contained in PSPACE and NP, respectively. Second, we show that the existence of an equilibrium with a binary payoff (i.e. an equilibrium where each player either wins or loses with probability 1) is decidable. We also establish that the existence of a Nash equilibrium with a certain binary payoff entails the existence of an equilibrium with the same payoff in pure, finite-state strategies.

  @inproceedings{UW09a,
       author = {Michael Ummels and Dominik Wojtczak},
       title = {Decision Problems for Nash Equilibria in Stochastic Games},
       booktitle = {Proceedings of the 18th Annual Conference of the European Association for Computer Science Logic, CSL '09},
       publisher = {Springer-Verlag},
       note = {To appear},
       url = {http://www.logic.rwth-aachen.de/~ummels/csl09.pdf},
  }
  

• M. Ummels and D. Wojtczak. The Complexity of Nash Equilibria in Simple Stochastic Multiplayer Games. In Proceedings of the 36th International Colloquium on Automata, Languages and Programming, ICALP 2009. Springer-Verlag. To appear.                                 
  Abstract   BibTeX

  We analyse the computational complexity of finding Nash equilibria in simple stochastic multiplayer games. We show that restricting the search space to equilibria whose payoffs fall into a certain interval may lead to undecidability. In particular, we prove that the following problem is undecidable: Given a game G, does there exist a pure-strategy Nash equilibrium of G where player 0 wins with probability 1. Moreover, this problem remains undecidable if it is restricted to strategies with (unbounded) finite memory. However, if mixed strategies are allowed, decidability remains an open problem. One way to obtain a provably decidable variant of the problem is to restrict the strategies to be positional or stationary. For the complexity of these two problems, we obtain a common lower bound of NP and upper bounds of NP and PSPACE respectively.

  @inproceedings{UW09,
       author = {Michael Ummels and Dominik Wojtczak},
       title = {The Complexity of Nash Equilibria in Simple Stochastic Multiplayer Games},
       booktitle = {Proceedings of the 36th International Colloquium on Automata, Languages and Programming, ICALP 2009},
       publisher = {Springer-Verlag},
       note = {To appear},
       url = {http://www.logic.rwth-aachen.de/~ummels/icalp09.pdf},
  }
  

2009

• D. Fischer, E. Grädel, and Ł. Kaiser. Model Checking Games for the Quantitative $\mu$-Calculus. Theory of Computing Systems, 2009.                                 
  Abstract   BibTeX

  We investigate quantitative extensions of modal logic and the modal $\mu$-calculus, and study the question whether the tight connection between logic and games can be lifted from the qualitative logics to their quantitative counterparts. It turns out that, if the quantitative $\mu$-calculus is defined in an appropriate way respecting the duality properties between the logical operators, then its model checking problem can indeed be characterised by a quantitative variant of parity games. However, these quantitative games have quite different properties than their classical counterparts, in particular they are, in general, not positionally determined. The correspondence between the logic and the games goes both ways: the value of a formula on a quantitative transition system coincides with the value of the associated quantitative game, and conversely, the values of quantitative parity games are definable in the quantitative $\mu$-calculus.

  @article{FGK09,
       author = {Diana Fischer and Erich Grädel and Łukasz Kaiser},
       title = {Model Checking Games for the Quantitative $\mu$-Calculus},
       journal = {Theory of Computing Systems},
       year = {2009},
       note = {Special Issue of STACS 2008},
       annote = {Online First},
       url = {http://www.springerlink.com/content/qj8p74228863m451/?p=106a29476a5b4d5b99663401ae6ad229&pi=3},
  }
  

2008

• D. Berwanger, K. Chatterjee, L. Doyen, T. A. Henzinger, and S. Raje. Strategy Construction for Parity Games with Imperfect Information. In Proceedings of the 19th International Conference on Concurrency Theory, CONCUR 2008, vol. 5201 of LNCS, pp. 325-339. Springer-Verlag, 2008.                                 
  Abstract   BibTeX

  We consider imperfect-information parity games in which strategies rely on observations that provide imperfect information about the history of a play. To solve such games, i.e., to determine the winning regions of players and corresponding winning strategies, one can use the subset construction to build an equivalent perfect-information game. Recently, an algorithm that avoids the inefficient subset construction has been proposed. The algorithm performs a fixed-point computation in a lattice of antichains, thus maintaining a succinct representation of state sets. However, this representation does not allow to recover winning strategies. In this paper, we build on the antichain approach to develop an algorithm for constructing the winning strategies in parity games of imperfect information. We have implemented this algorithm as a prototype. To our knowledge, this is the first implementation of a procedure for solving imperfect-information parity games on graphs.

  @inproceedings{BerwangerCDHR08,
       author = {Dietmar Berwanger and Krishnendu Chatterjee and Laurent Doyen and Thomas A. Henzinger and Sangram Raje},
       title = {Strategy Construction for Parity Games with Imperfect Information},
       booktitle = {Proceedings of the 19th International Conference on Concurrency Theory, CONCUR 2008},
       year = {2008},
       pages = {325-339},
       ee = {http://dx.doi.org/10.1007/978-3-540-85361-9_27},
       publisher = {Springer-Verlag},
       series = {LNCS},
       volume = {5201},
       url = {http://www.logic.rwth-aachen.de/pub/dwb/concur08.pdf},
  }
  

• V. Bárány. A Hierarchy of Automatic $\omega$-Words having a Decidable MSO Theory. RAIRO - Theor. Inf. Appl., vol. 42, pp. 417-450, 2008.                                 
  Abstract   BibTeX

  We investigate automatic presentations of omega-words. Starting points of our study are the works of Rigo and Maes, Caucal, and Carton and Thomas concerning lexicographic presentation, MSO-interpretability in algebraic trees, and the decidability of the MSO theory of morphic words. Refining their techniques we observe that the lexicographic presentation of a (morphic) word is in a certain sense canonical. We then generalize our techniques to a hierarchy of classes of omega-words enjoying the above mentioned definability and decidability properties. We introduce k-lexicographic presentations, and morphisms of level k stacks and show that these are inter-translatable, thus giving rise to the same classes of k-lexicographic or level k morphic words. We prove that these presentations are also canonical, which implies decidability of the MSO theory of every k-lexicographic word as well as closure of these classes under MSO-definable recolorings, e.g. closure under deterministic sequential mappings. The classes of k-lexicographic words are shown to constitute an infinite hierarchy.

  @article{Bar08ITA,
       author = {Vince Bárány},
       title = {A Hierarchy of Automatic $\omega$-Words having a Decidable MSO Theory},
       journal = {RAIRO - Theor. Inf. Appl.},
       volume = {42},
       pages = {417-450},
       year = {2008},
       doi = {10.1051/ita:2008008},
       url = {http://www.logic.rwth-aachen.de/~vbarany/hom_ITA.pdf},
  }
  

• A. Dawar and E. Grädel. The Descriptive Complexity of Parity Games. In Proceedings of the 17th Annual Conference on Computer Science Logic, CSL 2008, vol. 5213 of LNCS, pp. 354–368. Springer-Verlag, 2008.                                 
  Abstract   BibTeX

  We study the logical definablity of the winning regions of parity games. For games with a bounded number of priorities, it is wellknown that the winning regions are definable in the modal mu-calculus. Here we investigate the case of an unbounded number of priorities, both for finite game graphs and for arbitrary ones. In the general case, winning regions are definable in guarded second-order logic (GSO), but not in least-fixed point logic (LFP). On finite game graphs, winning regions are LFP-definable if, and only if, they are computable in polynomial time, and this result extends to any class of finite games that is closed under taking bisimulation quotients.

  @inproceedings{DG08,
       author = {Anuj Dawar and Erich Grädel},
       title = {The Descriptive Complexity of Parity Games},
       booktitle = {Proceedings of the 17th Annual Conference on Computer Science Logic, CSL 2008},
       pages = {354–368},
       series = {LNCS},
       volume = {5213},
       publisher = {Springer-Verlag},
       year = {2008},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/csl08.pdf},
  }
  

• D. Fischer, E. Grädel, and Ł. Kaiser. Model Checking Games for the Quantitative $\mu$-Calculus. In Proceedings of the 25th International Symposium on Theoretical Aspects of Computer Science, STACS 2008 (S. Albers and P. Weil, Eds.), pp. 301–312, 2008.                                 
  Abstract   BibTeX

  We investigate quantitative extensions of modal logic and the modal $\mu$-calculus, and study the question whether the tight connection between logic and games can be lifted from the qualitative logics to their quantitative counterparts. It turns out that, if the quantitative $\mu$-calculus is defined in an appropriate way respecting the duality properties between the logical operators, then its model checking problem can indeed be characterised by a quantitative variant of parity games. However, these quantitative games have quite different properties than their classical counterparts, in particular they are, in general, not positionally determined. The correspondence between the logic and the games goes both ways: the value of a formula on a quantitative transition system coincides with the value of the associated quantitative game, and conversely, the values of quantitative parity games are definable in the quantitative $\mu$-calculus.

  @inproceedings{FGK08,
       author = {Diana Fischer and Erich Grädel and Łukasz Kaiser},
       title = {Model Checking Games for the Quantitative $\mu$-Calculus},
       booktitle = {Proceedings of the 25th International Symposium on Theoretical Aspects of Computer Science, STACS 2008},
       editor = {Susanne Albers and Pascal Weil},
       pages = {301–312},
       year = {2008},
  }
  

• T. Ganzow and S. Rubin. Order-Invariant MSO is Stronger than Counting MSO in the Finite. In Proceedings of the 25th International Symposium on Theoretical Aspects of Computer Science, STACS 2008 (S. Albers and P. Weil, Eds.), pp. 313–324, 2008.                                 
  Abstract   BibTeX

  We compare the expressiveness of two extensions of monadic second-order logic (MSO) over the class of finite structures. The first, counting monadic second-order logic (CMSO), extends MSO with first-order modulo-counting quantifiers, allowing the expression of queries like ``the number of elements in the structure is even''. The second extension allows the use of an additional binary predicate, not contained in the signature of the queried structure, that must be interpreted as an arbitrary linear order on its universe, obtaining order-invariant MSO. While it is straightforward that every CMSO formula can be translated into an equivalent order-invariant MSO formula, the converse had not yet been settled. Courcelle showed that for restricted classes of structures both order-invariant MSO and CMSO are equally expressive, but conjectured that, in general, order-invariant MSO is stronger than CMSO. We affirm this conjecture by presenting a class of structures that is order-invariantly definable in MSO but not definable in CMSO.

  @inproceedings{GR08,
       author = {Tobias Ganzow and Sasha Rubin},
       title = {Order-Invariant MSO is Stronger than Counting MSO in the Finite},
       booktitle = {Proceedings of the 25th International Symposium on Theoretical Aspects of Computer Science, STACS 2008},
       editor = {Susanne Albers and Pascal Weil},
       pages = {313–324},
       year = {2008},
       url = {http://www.logic.rwth-aachen.de/pub/ganzow/GR-STACS08.pdf},
  }
  

• E. Grädel. Banach-Mazur Games on Graphs. In Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2008 (R. Hariharan, M. Mukund, and V. Vinay, Eds.), Dagstuhl, Germany. Schloss Dagstuhl – Leibniz-Zentrum fuer Informatik, Germany, 2008.                                 
  Abstract   BibTeX

  We survey determinacy, definability, and complexity issues of Banach-Mazur games on finite and infinite graphs. Infinite games where two players take turns to move a token through a directed graph, thus tracing out an infinite path, have numerous applications in different branches of mathematics and computer science. In the usual format, the possible moves of the players are given by the edges of the graph; in each move a player takes the token from its current position along an edge to a next position. In Banach-Mazur games the players instead select in each move a path of arbitrary finite length rather than just an edge. In both cases the outcome of a play is an infinite path. A winning condition is thus given by a set of infinite paths which is often specified by a logical formula, for instance from S1S, LTL, or first-order logic. Banach-Mazur games have a long tradition in descriptive set theory and topology, and they have recently been shown to have interesting applications also in computer science, for instance for planning in nondeterministic domains, for the study of fairness in concurrent systems, and for the semantics of timed automata. It turns out that Banach-Mazur games behave quite differently than the usual graph games. Often they admit simpler winning strategies and more efficient algorithmic solutions. For instance, Banach-Mazur games with omega-regular winning conditions always have positional winning strategies, and winning positions for finite Banach-Mazur games with Muller winning condition are computable in polynomial time.

  @inproceedings{Graedel08,
       author = {Erich Grädel},
       title = {Banach-Mazur Games on Graphs},
       booktitle = {Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2008},
       year = {2008},
       editor = {Ramesh Hariharan and Madhavan Mukund and V. Vinay},
       publisher = {Schloss Dagstuhl – Leibniz-Zentrum fuer Informatik, Germany},
       address = {Dagstuhl, Germany},
       url = {http://drops.dagstuhl.de/opus/volltexte/2008/1768},
       annote = {Keywords: Games, strategies, determinacy, positional determinacy, definability, complexity},
  }
  

• E. Grädel and M. Ummels. Solution Concepts and Algorithms for Infinite Multiplayer Games. In New Perspectives on Games and Interaction (K. Apt and R. van Rooij, Eds.), vol. 4 of Texts in Logic and Games, pp. 151–178. Amsterdam University Press, 2008.                                 
  Abstract   BibTeX

  We survey and discuss several solution concepts for infinite turn-based multiplayer games with qualitative (i.e. win-lose) objectives of the players. These games generalise in a natural way the common model of games in verification which are two-player, zero-sum games with $\omega$-regular winning conditions. The generalisation is in two directions: our games may have more than two players, and the objectives of the players need not be completely antagonistic. The notion of a Nash equilibrium is the classical solution concept in game theory. However, for games that extend over time, in particular for games of infinite duration, Nash equilibria are not always satisfactory as a notion of rational behaviour. We therefore discuss variants of Nash equilibria such as subgame perfect equilibria and secure equilibria. We present criteria for the existence of Nash equilibria and subgame perfect equilibria in the case of arbitrary many players and for the existence of secure equilibria in the two-player case. In the second part of this paper, we turn to algorithmic questions: For each of the solution concepts that we discuss, we present algorithms that decide the existence of a solution with certain requirements in a game with parity winning conditions. Since arbitrary $\omega$-regular winning conditions can be reduced to parity conditions, our algorithms are also applicable to games with arbitrary $\omega$-regular winning conditions.

  @inproceedings{GU08,
       author = {Erich Grädel and Michael Ummels},
       title = {Solution Concepts and Algorithms for Infinite Multiplayer Games},
       booktitle = {New Perspectives on Games and Interaction},
       editor = {Krzysztof Apt and Robert van Rooij},
       series = {Texts in Logic and Games},
       volume = {4},
       publisher = {Amsterdam University Press},
       pages = {151–178},
       year = {2008},
       url = {http://www.logic.rwth-aachen.de/~ummels/knaw07.pdf},
  }
  

• Ł. Kaiser. Logic and Games on Automatic Structures. PhD thesis, RWTH Aachen, 2008.                                 
  Abstract   BibTeX

  The evaluation of a logical formula can be viewed as a game played by two opponents, one trying to show that the formula is true and the other trying to prove it false. This correspondence is exploited algorithmically to evaluate formulas of first and second-order logic on finite structures. We extend the game-based algorithmic approach to first-order logic on infinite structures that arise in computer science. Such structures are stored and manipulated by a computer, thus elements and relations must be represented in a finite way. We study a prominent class of finitely presentable structures, namely automatic structures.

  Automatic structures consist of elements represented by words over a finite alphabet. Relations within these structures are represented by synchronous automata that perform step-by-step transitions on tuples of symbols from the alphabet. A prominent example of an automatic structure is Presburger arithmetic, for which the natural way of writing numbers as sequences of digits and the standard column addition method constitute an automatic presentation.

  An important property of automatic structures is that first-order logic is decidable on these structures. To develop the correspondence between games and logic on automatic structures, we first look for suitable extensions of first-order logic that remain decidable. We study the notion of game quantification and extend the notions of open and closed game quantifiers, introduced in the model theory of infinitary logics, to a regular game quantifier. We show that this game quantifier preserves regularity on automatic presentations and investigate its expressive power. We identify the classes of structures on which first-order logic extended with this quantifier collapses to pure first-order logic. For better understanding of the classes where this is not the case, we introduce the notion of inductive automorphisms and show that they preserve relations defined using the game quantifier.

  Model-checking games for the above extension of first-order logic can be defined in a more natural way than for pure first-order logic. Towards this, we extend the classical two-player parity games to a multiplayer setting where two coalitions play against each other with a particular kind of hierarchical imperfect information about actions of the players. In contrast to the classical case, in hierarchical games it is essential that players alternate. We show that otherwise the problem which coalition wins a hierarchical game is undecidable. Nevertheless, there is an important aspect in which they are similar to classical games: hierarchical games are robust with respect to changes of the representation of winning condition.

  One reason for this robustness of hierarchical games is that only a finite memory is needed to reduce games with complex winning conditions to games with simpler ones. While this technique has been well-known for games with finitely many priorities, our approach is the first to extend it to games with infinitely many priorities on infinite arenas. We generalize the classical notion of latest appearance record to a new memory structure, which we show to be sufficient for winning Muller games with a finite or co-finite number of sets in the Muller condition, and additionally for a few other classes of games with infinitely many priorities. Certain classes of winning conditions on infinitely many priorities admit descriptions in terms of generalized Zielonka trees. We investigate such conditions and show that the correspondence between the number of branches of a Zielonka tree and the memory needed for strategies generalizes to the case of infinitely many priorities.

  A basic way of extending first-order logic is by adding generalized Lindström quantifiers. We address the following question: which generalized unary quantifiers can be added to first-order logic without introducing non-regular relations on automatic structures. We answer this question by giving a complete characterization of such quantifiers in terms of definability using cardinality and modulo counting quantifiers. We show that these quantifiers indeed preserve regularity on all automatic structures, including the non-injective omega-automatic ones. As a corollary we answer a question of Blumensath and prove that all countable omega-automatic structures are in fact finite-word automatic. Further, we study cardinality quantifiers on a large class of generalized-automatic structures. We use the composition method for monadic second-order logic to show that on such structures cardinality quantifiers collapse to first-order logic.

  @phdthesis{Kaiser08,
       author = {Łukasz Kaiser},
       title = {Logic and Games on Automatic Structures},
       year = {2008},
       school = {RWTH Aachen},
       type = {Ph.D. Thesis},
       url = {http://www.logic.rwth-aachen.de/~kaiser/diss.pdf},
  }
  

• Ł. Kaiser, S. Rubin, and V. Bárány. Cardinality and counting quantifiers on omega-automatic structures. In Proceedings of the 25th International Symposium on Theoretical Aspects of Computer Science, STACS 2008 (S. Albers and P. Weil, Eds.), pp. 385–396, 2008.                                 
  Abstract   BibTeX

  We investigate structures that can be represented by omega-automata, so called omega-automatic structures, and prove that relations defined over such structures in first-order logic expanded by the first-order quantifiers `there exist at most $\aleph_0$ many', 'there exist finitely many' and 'there exist $k$ modulo $m$ many' are omega-regular. The proof identifies certain algebraic properties of omega-semigroups. As a consequence an omega-regular equivalence relation of countable index has an omega-regular set of representatives. This implies Blumensath's conjecture that a countable structure with an $\omega$-automatic presentation can be represented using automata on finite words. This also complements a very recent result of Hjörth, Khoussainov, Montalban and Nies showing that there is an omega-automatic structure which has no injective presentation.

  @inproceedings{BKR08,
       author = {Łukasz Kaiser and Sasha Rubin and Vince Bárány},
       title = {Cardinality and counting quantifiers on omega-automatic structures},
       booktitle = {Proceedings of the 25th International Symposium on Theoretical Aspects of Computer Science, STACS 2008},
       editor = {Susanne Albers and Pascal Weil},
       url = {http://www.logic.rwth-aachen.de/~kaiser/cardinality_automatic.pdf},
       pages = {385–396},
       year = {2008},
  }
  

• R. Rabinovich. Complexity Measures of Directed Graphs. Diploma thesis, RWTH-Aachen, 2008.             
  BibTeX

  @misc{Rabinovich08,
       author = {Roman Rabinovich},
       title = {Complexity Measures of Directed Graphs},
       howpublished = {Diploma thesis, RWTH-Aachen},
       year = {2008},
       url = {http://logic.rwth-aachen.de/People/Rabinovich/diplomarbeit.pdf},
  }
  

• M. Ummels. The Complexity of Nash Equilibria in Infinite Multiplayer Games. In Proceedings of the 11th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2008 (R. Amadio, Ed.), vol. 4962 of LNCS, pp. 20–34. Springer-Verlag, 2008.                                 
  Abstract   BibTeX

  We study the complexity of Nash equilibria in infinite (turn-based, qualitative) multiplayer games. Chatterjee et al. showed the existence of a Nash equilibrium in any such game with $\omega$-regular winning conditions, and they devised an algorithm for computing one. We argue that in applications it is often insufficient to compute just some Nash equilibrium. Instead, we enrich the problem by allowing to put (qualitative) constraints on the payoff of the desired equilibrium. Our main result is that the resulting decision problem is NP-complete for games with co-Büchi, parity or Streett winning conditions but fixed-parameter tractable for many natural restricted classes of games with parity winning conditions. For games with Büchi winning conditions we show that the problem is, in fact, decidable in polynomial time. We also analyse the complexity of strategies realising a Nash equilibrium. In particular, we show that pure finite-state strategies as opposed to arbitrary mixed strategies suffice to realise any Nash equilibrium of a game with $\omega$-regular winning conditions with a qualitative constraint on the payoff.

  @inproceedings{Ummels08,
       author = {Michael Ummels},
       title = {The Complexity of Nash Equilibria in Infinite Multiplayer Games},
       booktitle = {Proceedings of the 11th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2008},
       editor = {Roberto Amadio},
       publisher = {Springer-Verlag},
       series = {LNCS},
       volume = {4962},
       pages = {20–34},
       year = {2008},
       url = {http://www.logic.rwth-aachen.de/~ummels/fossacs08.pdf},
  }
  

2007

• D. Berwanger, E. Grädel, and G. Lenzi. The variable hierarchy of the $\mu$-calculus is strict. Theory of Computing Systems, vol. 40, pp. 437–466, 2007.                                 
  Abstract   BibTeX

  Most of the logics commonly used in verification, such as LTL, CTL, CTL*, and PDL can be embedded into the two-variable fragment of the mu-calculus. It is also known that properties occurring at arbitrarily high levels of the alternation hierarchy can be formalised using only two variables. This raises the question whether the number of fixedpoint variables in mu-formulae can be bounded in general.

  We answer this question negatively, and prove that the variable-hierarchy of the mu-calculus is semantically strict. For any k, we provide examples of formulae with k variables that are not equivalent to any formula with fewer variables. In particular, this implies that Parikh's Game Logic is less expressive than the mu-calculus, thus resolving an open issue raised by Parikh in 1983.

  @article{BGL07,
       author = {Dietmar Berwanger and Erich Grädel and Giacomo Lenzi},
       title = {The variable hierarchy of the $\mu$-calculus is strict},
       journal = {Theory of Computing Systems},
       volume = {40},
       pages = {437–466},
       year = {2007},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/BeGrLe-tocs07.pdf},
  }
  

• D. Berwanger. Admissibility in infinite games. In Proceedings of the 24th Annual Symposium on Theoretical Aspects of Computer Science, STACS 2007 (W. Thomas and P. Weil, Eds.), vol. 4393 of LNCS, pp. 188–199. Springer-Verlag, 2007.             
  BibTeX

  @inproceedings{Berwanger07,
       author = {Dietmar Berwanger},
       title = {Admissibility in infinite games},
       booktitle = {Proceedings of the 24th Annual Symposium on Theoretical Aspects of Computer Science, STACS 2007},
       editor = {Wolfgang Thomas and Pascal Weil},
       publisher = {Springer-Verlag},
       series = {LNCS},
       volume = {4393},
       pages = {188–199},
       year = {2007},
       url = {http://www.logic.rwth-aachen.de/~dwb/admissibility.pdf},
  }
  

• V. Bárány. Automatic Presentations of Infinite Structures. PhD thesis, RWTH Aachen, 2007.             
  BibTeX

  @phdthesis{Bar07diss,
       author = {V. Bárány},
       title = {Automatic Presentations of Infinite Structures},
       school = {RWTH Aachen},
       type = {Dissertation},
       year = {2007},
       url = {http://www.logic.rwth-aachen.de/~vbarany/diss.pdf},
  }
  

• J. Flum, E. Grädel, and T. Wilke (Eds.). Logic and Automata: History and Perspectives. Amsterdam University Press, 2007.             
  BibTeX

  @book{FlumGraWil07,
       editor = {J. Flum and E. Grädel and T. Wilke},
       title = {Logic and Automata: History and Perspectives},
       publisher = {Amsterdam University Press},
       year = {2007},
       series = {Texts in Logic and Games},
       volume = {2},
       url = {http://www.logic.rwth-aachen.de/Books/},
  }
  

• E. Grädel. Finite Model Theory and Descriptive Complexity. In Finite Model Theory and Its Applications, pp. 125–230. Springer-Verlag, 2007.             
  BibTeX

  @incollection{Graedel03,
       author = {E. Grädel},
       title = {Finite Model Theory and Descriptive Complexity},
       booktitle = {Finite Model Theory and Its Applications},
       publisher = {Springer-Verlag},
       year = {2007},
       pages = {125–230},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/FMTbook-Chapter3.pdf},
  }
  

• E. Grädel and Ł. Kaiser. What kind of memory is needed to win infinitary Muller games? In Interactive Logic (J. van Benthem, B. Löwe, and D. Gabbay, Eds.), vol. 1 of Texts in Logic and Games. Amsterdam University Press, 2007.                                 
  Abstract   BibTeX

  In an influential paper entitled ``How much memory is needed to win infinite games'', Dziembowski, Jurdziński, and Walukiewicz have shown that there are Muller games of size $O(n)$ whose winning strategies require memory of size at least $n!$. This shows that the LAR-memory, based on the latest appearance records introduced by Gurevich and Harrington, is optimal for solving Muller games. We review these results and reexamine the situation for the case of infinitary Muller games, i.e. Muller games with infinitely many priorities. We introduce a new, infinite, memory structure, based on finite appearance records (FAR) and investigate classes of Muller games that can be solved with FAR-memory.

  @inproceedings{GK07,
       author = {Erich Grädel and Łukasz Kaiser},
       title = {What kind of memory is needed to win infinitary Muller games?},
       editor = {Johan van Benthem and Benedikt Löwe and Dov Gabbay},
       booktitle = {Interactive Logic},
       series = {Texts in Logic and Games},
       volume = {1},
       publisher = {Amsterdam University Press},
       year = {2007},
       url = {http://www.logic.rwth-aachen.de/pub/kaiser/memory_kinds.pdf},
  }
  

• E. Grädel, P. G. Kolaitis, L. Libkin, M. Marx, J. Spencer, M. Y. Vardi, Y. Venema, and S.Weinstein. Finite Model Theory and Its Applications. Springer-Verlag, 2007.             
  BibTeX

  @book{FMT07,
       author = {E. Grädel and Ph. G. Kolaitis and L. Libkin and M. Marx and J. Spencer and M. Y. Vardi and Y. Venema and S.Weinstein},
       title = {Finite Model Theory and Its Applications},
       publisher = {Springer-Verlag},
       year = {2007},
       series = {Texts in Theoretical Computer Science},
       url = {http://www.logic.rwth-aachen.de/Books/},
  }
  

2006

• D. Berwanger, A. Dawar, P. Hunter, and S. Kreutzer. DAG-width and parity games. In Proceedings of the 23rd Annual Symposium on Theoretical Aspects of Computer Science, STACS 2006, vol. 3884 of LNCS, pp. 524–536. Springer-Verlag, 2006.             
  BibTeX

  @inproceedings{BDHK06,
       author = {Dietmar Berwanger and Anuj Dawar and Paul Hunter and Stephan Kreutzer},
       title = {DAG-width and parity games},
       booktitle = {Proceedings of the 23rd Annual Symposium on Theoretical Aspects of Computer Science, STACS 2006},
       publisher = {Springer-Verlag},
       series = {LNCS},
       volume = {3884},
       year = {2006},
       pages = {524–536},
       url = {http://www.logic.rwth-aachen.de/~dwb/pub/dagwidth.pdf},
  }
  

• D. Berwanger and D. Janin. Automata on Directed Graphs: Vertex versus Edge Marking. In Proceedings of the 3rd International Conference on Graph Transformation, ICGT 2006, vol. 4179 of LNCS, pp. 46–60. Springer-Verlag, 2006.             
  BibTeX

  @inproceedings{BerwangerJan06,
       author = {Dietmar Berwanger and David Janin},
       title = {Automata on Directed Graphs: Vertex versus Edge Marking},
       booktitle = {Proceedings of the 3rd International Conference on Graph Transformation, ICGT 2006},
       url = {http://www.logic.rwth-aachen.de/~dwb/pub/acc.pdf},
       publisher = {Springer-Verlag},
       series = {LNCS},
       volume = {4179},
       pages = {46–60},
       year = {2006},
  }
  

• V. Bárány. A Hierarchy of Automatic Words having a Decidable MSO Theory. In Online Proceedings of the 11th Journées Montoises, Rennes (D. Caucal, Ed.), 2006.                                 
  Abstract   BibTeX

  We investigate automatic presentations of infinite words. Starting points of our study are the works of Rigo and Maes, and Carton and Thomas concerning the lexicographic presentation, respectively the decidability of the MSO theory of morphic words. Refining their techniques we observe that the lexicographic presentation of a (morphic) word is canonical in a certain sense. We then go on to generalize our techniques to a hierarchy of classes of infinite words enjoying the above mentioned properties. We introduce $k$-lexicographic presentations, and morphisms of level $k$ stacks and show that these are inter-translatable, thus giving rise to the same classes of $k$-lexicographic or level $k$ morphic words. We prove that these presentations are also canonical, which implies decidability of the MSO theory of every $k$-lexicographic word as well as closure of these classes under restricted MSO interpretations, e.g. closure under deterministic sequential mappings. The classes of $k$-lexicographic words are shown to form an infinite hierarchy.

  @inproceedings{Bar06JM,
       author = {Vince Bárány},
       title = {A Hierarchy of Automatic Words having a Decidable MSO Theory},
       year = {2006},
       booktitle = {Online Proceedings of the 11th Journées Montoises, Rennes},
       editor = {D. Caucal},
       url = {http://www.logic.rwth-aachen.de/~vbarany/jm06.pdf},
  }
  

• V. Bárány, C. Löding, and O. Serre. Regularity Problems for Visibly Pushdown Languages. In Proceedings of the 23rd Annual Symposioum on Theoretical Aspects of Computer Science, STACS 2006 (B. Durand and W. Thomas, Eds.), vol. 3884 of LNCS, pp. 420–431. Springer, 2006.                                 
  Abstract   BibTeX

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

  @inproceedings{BLS06STACS,
       author = {Vince Bárány and Christof Löding and Olivier Serre},
       title = {Regularity Problems for Visibly Pushdown Languages},
       year = {2006},
       booktitle = {Proceedings of the 23rd Annual Symposioum on Theoretical Aspects of Computer Science, STACS 2006},
       editor = {B. Durand and W. Thomas},
       series = {LNCS},
       volume = {3884},
       pages = {420–431},
       publisher = {Springer},
       url = {http://www.logic.rwth-aachen.de/~vbarany/BLS_stacs06_withAppendix.pdf},
  }
  

• V. Bárány. Invariants of Automatic Presentations and Semi-Synchronous Transductions. In Proceedings of the 23rd Annual Symposioum on Theoretical Aspects of Computer Science, STACS 2006 (B. Durand and W. Thomas, Eds.), vol. 3884 of LNCS, pp. 289–300. Springer, 2006.                                 
  Abstract   BibTeX

  Automatic structures are countable structures finitely presentable by a collection of automata. We study questions related to properties invariant with respect to the choice of an automatic presentation. We give a negative answer to a question of Rubin concerning definability of intrinsically regular relations by showing that order-invariant first-order logic can be stronger than first-order logic with counting on automatic structures. We introduce a notion of equivalence of automatic presentations, define semi-synchronous transductions, and show how these concepts correspond. Our main result is that a one-to-one function on words preserves regularity as well as non-regularity of all relations iff it is a semi-synchronous transduction. We also characterize automatic presentations of the complete structures of Blumensath and Grädel.

  @inproceedings{Bar06STACS,
       author = {Vince Bárány},
       title = {Invariants of Automatic Presentations and Semi-Synchronous Transductions},
       year = {2006},
       booktitle = {Proceedings of the 23rd Annual Symposioum on Theoretical Aspects of Computer Science, STACS 2006},
       editor = {B. Durand and W. Thomas},
       series = {LNCS},
       volume = {3884},
       pages = {289–300},
       publisher = {Springer},
       url = {http://www.logic.rwth-aachen.de/~vbarany/stacs06_88_appendix.pdf},
  }
  

• A. Dawar, E. Grädel, and S. Kreutzer. Backtracking Games and Inflationary Fixed Points. Theoretical Computer Science, vol. 350, pp. 174–187, 2006.                                 
  Abstract   BibTeX

  We define a new class of games, called backtracking games. Backtracking games are essentially parity games with an additional rule allowing players, under certain conditions, to return to an earlier position in the play and revise a choice or to force a countback of the number of moves. This new feature makes backtracking games more powerful than parity games. As a consequence, winning strategies become more complex objects and computationally harder. The corresponding increase in expressiveness allows us to use backtracking games as model-checking games for inflationary fixed-point logics such as IFP or MIC. We identify a natural subclass of backtracking games, the simple games, and show that these are the "right" model-checking games for IFP by (a) giving a translation of formulae $\phi$ and structures $A$ into simple games such that $A |= \phi$ if, and only if, Player 0 wins the corresponding game and (b) showing that the winner of simple backtracking games can again be defined in IFP.

  @article{DGK06,
       author = {Anuj Dawar and Erich Grädel and Stephan Kreutzer},
       title = {Backtracking Games and Inflationary Fixed Points},
       journal = {Theoretical Computer Science},
       year = {2006},
       volume = {350},
       pages = {174–187},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/DaGrKr-tcs05.ps},
  }
  

• E. Grädel and I. Walukiewicz. Positional Determinacy of Games with Infinitely Many Priorities. Logical Methods in Computer Science, 2006.                                 
  Abstract   BibTeX

  We study two-player games of infinite duration that are played on finite or infinite game graphs. A winning strategy for such a game is positional if it only depends on the current position, and not on the history of the play. A game is positionally determined if, from each position, one of the two players has a positional winning strategy.

  The theory of such games is well studied for winning conditions that are defined in terms of a mapping that assigns to each position a priority from a finite set C. Specifically, in Muller games the winner of a play is determined by the set of those priorities that have been seen infinitely often; an important special case are parity games where the least (or greatest) priority occurring infinitely often determines the winner. It is well-known that parity games are positionally determined whereas Muller games are determined via finite-memory strategies.

  In this paper, we extend this theory to the case of games with infinitely many priorities. Such games arise in several application areas, for instance in pushdown games with winning conditions depending on stack contents.

  For parity games there are several generalisations to the case of infinitely many priorities. While max-parity games over $\omega$ or min-parity games over larger ordinals than $\omega$ require strategies with infinite memory, we can prove that min-parity games with priorities in $\omega$ are positionally determined. Indeed, it turns out that the min-parity condition over $\omega$ is the only infinitary Muller condition that guarantees positional determinacy on all game graphs.

  @article{GraedelWal06,
       author = {E. Grädel and I. Walukiewicz},
       title = {Positional Determinacy of Games with Infinitely Many Priorities},
       journal = {Logical Methods in Computer Science},
       year = {2006},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/GrWa-lmcs06.pdf},
  }
  

• Ł. Kaiser. Game Quantification on Automatic Structures and Hierarchical Model Checking Games. In Proceedings of the 15th Annual Conference on Computer Science Logic, CSL 2006 (Z. Esik, Ed.), vol. 4207 of LNCS, pp. 411–425. Springer-Verlag, 2006.                                 
  Abstract   BibTeX

  Game quantification is an expressive concept and has been studied in model theory and descriptive set theory, especially in relation to infinitary logics. Automatic structures on the other hand appear very often in computer science, especially in program verification. We extend first-order logic on structures on words by allowing to use an infinite string of alternating quantifiers on letters of a word, the game quantifier. This extended logic is decidable and preserves regularity on automatic structures, but can be undecidable on other structures even with decidable first-order theory. We show that in the presence of game quantifier any relation that allows to distinguish successors is enough to define all regular relations and therefore the game quantifier is strictly more expressive than first-order logic in such cases. Conversely, if there is an automorphism of atomic relations that swaps some successors then we prove that it can be extended to any relations definable with game quantifier. After investigating it's expressiveness, we use game quantification to introduce a new type of combinatorial games with multiple players and imperfect information exchanged with respect to a hierarchical constraint. It is shown that these games on finite arenas exactly capture the logic with game quantifier when players alternate their moves but are undecidable and not necessarily determined in the other case. In this way we define the first model checking games with finite arenas that can be used for model checking first-order logic on automatic structures.

  @inproceedings{K06,
       author = {Łukasz Kaiser},
       title = {Game Quantification on Automatic Structures and Hierarchical Model Checking Games},
       booktitle = {Proceedings of the 15th Annual Conference on Computer Science Logic, CSL 2006},
       publisher = {Springer-Verlag},
       series = {LNCS},
       editor = {Zoltan Esik},
       volume = {4207},
       pages = {411–425},
       year = {2006},
       url = {http://www.logic.rwth-aachen.de/pub/kaiser/game_quantifier_logic.pdf},
  }
  

• M. Ummels. Rational Behaviour and Strategy Construction in Infinite Multiplayer Games. In Proceedings of the 26th International Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2006 (S. Arun-Kumar and N. Garg, Eds.), vol. 4337 of LNCS, pp. 212–223. Springer-Verlag, 2006.                                 
  Abstract   BibTeX

  We study infinite games played by arbitrarily many players on a directed graph. Equilibrium states capture rational behaviour in these games. Instead of the well-known notion of a Nash equilibrium, we focus on the notion of a subgame perfect equilibrium. We argue that the latter one is more appropriate for the kind of games we study, and we show the existence of a subgame perfect equilibrium in any infinite game with $\omega$-regular winning conditions. As, in general, equilibria are not unique, it is appealing to compute one with a maximal payoff. This problem corresponds naturally to the problem of deciding given a game and two payoff vectors whether the game has an equilibrium with a payoff in between the given thresholds. We show that this problem is decidable for games with $\omega$-regular winning conditions played on a finite graph and analyse its complexity. Moreover, we establish that any subgame perfect equilibrium of a game with $\omega$-regular winning conditions played on a finite graph can be implemented by finite-state strategies. Finally, we consider logical definability. We state that if we fix the number of players together with an $\omega$-regular winning condition for each of them and two payoff vectors the property that a game has a subgame perfect equilibrium with a payoff in between the given thresholds is definable in the modal $\mu$-calculus.

  @inproceedings{Ummels06,
       author = {Michael Ummels},
       title = {Rational Behaviour and Strategy Construction in Infinite Multiplayer Games},
       year = {2006},
       booktitle = {Proceedings of the 26th International Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2006},
       publisher = {Springer-Verlag},
       editor = {S. Arun-Kumar and Naveen Garg},
       series = {LNCS},
       volume = {4337},
       pages = {212–223},
       url = {http://www.logic.rwth-aachen.de/~ummels/fsttcs06.pdf},
  }
  

2005

• D. Berwanger. Games and Logical Expressiveness. PhD thesis, RWTH Aachen, 2005.                                 
  Abstract   BibTeX

  We investigat the inner structure of process logics, in particular of the mu-calculus $L_\mu$, from the viewpoint of games over graphs. First, we show that Parikh's Game Logic, a two-variable sublogic of the mu-calculus, is expressive enough to capture parity games and, hence, to reach arbitrarily high levels of the $L_\mu$ alternation hierarchy. Further, we devise a game that captures relevant issues of descriptive and computational complexity of the mu-calculus. As a first application, we show that, for the model-checking problem of $L_\mu$, our game naturally leads to instances that can be solved in polynomial time. On the basis of this game, we also derive a parameter that captures the number of variables required to specify the behaviour of a given transition system in the mu-calculus. As a consequence, it follows that the expressive power of the mu-calculus strictly increases with the number of variables used in formulae. Already a particular case of this result, that three variables can express more than two, allows us to separate the expressive power of Parikh's Game Logic and the mu-calculus, a question that was open since 1983.

  @phdthesis{BerwangerThesis,
       author = {Dietmar Berwanger},
       title = {Games and Logical Expressiveness},
       school = {RWTH Aachen},
       year = {2005},
       task = {2,7},
       url = {http://www.logic.rwth-aachen.de/pub/dwb/express.pdf},
  }
  

• D. Berwanger and E. Grädel. Entanglement – A Measure for the Complexity of Directed Graphs with Applications to Logic and Games. In Proceedings of LPAR 2004, Montevideo, Uruguay, vol. 3452 of LNCS, pp. 209–223. Springer-Verlag, 2005.                                 
  Abstract   BibTeX

  We propose a new parameter for the complexity of finite directed graphs which measures to what extent the cycles of the graph are intertwined. This measure, called entanglement, is defined by way of a game that is similar in spirit to the robber and cops games used to describe tree width, directed tree width, and hypertree width. Nevertheless on many classes of graphs, there are significant differences between entanglement and the various incarnations of tree width.

  As we will show, entanglement is intimately related to the descriptive complexity of the modal $\mu$-calculus. Particular, if we view the syntax of a formula as a tree with back edges leading from fixed-point variables to their definition, the block width of this syntax graph is bounded by the number of distinct variables used in the formula. On the one hand, the entanglement of a finite transition system provides an upper bound for the number of fixed point variables needed to describe it up to bisimulation.

  In addition to this, we prove that parity games of bounded entanglement can be solved in polynomial time. Specifically, we establish that the complexity of solving a parity game can be parametrised in terms of the minimal entanglement of subgames induced by winning strategies.

  @inproceedings{BerwangerGraLPAR04,
       author = {Dietmar Berwanger and Erich Grädel},
       title = {Entanglement – A Measure for the Complexity of Directed Graphs with Applications to Logic and Games},
       pages = {209–223},
       booktitle = {Proceedings of LPAR 2004, Montevideo, Uruguay},
       publisher = {Springer-Verlag},
       series = {LNCS},
       volume = {3452},
       year = {2005},
       url = {http://www.logic.rwth-aachen.de/pub/dwb/BG_lpar04.pdf},
       task = {2},
  }
  

• D. Berwanger and G. Lenzi. The variable hierarchy of the $\mu$-calculus is strict. In STACS 2005, Proceedings of the 22nd Symposium on Theoretical Aspects of Computer Science, vol. 3404 of LNCS, pp. 97–109. Springer-Verlag, 2005.                                 
  Abstract   BibTeX

  The modal $\mu$-calculus $\Lmu$ attains high expressive power by extending basic modal logic with monadic variables and binding them to extremal fixed points of definable operators. The number of variables occurring in a formula provides a relevant measure of its conceptual complexity. In a previous paper with Erich Grädel we have shown, for the existential fragment of $\Lmu$, that this conceptual complexity is also reflected in an increase of semantic complexity, by providing examples of existential formulae with $k$ variables that are not equivalent to any existential formula with fewer than $k$ variables.

  In this paper, we prove an existential preservation theorem for the family of $\Lmu$-formulae over at most $k$ variables that define simulation closures of finite strongly connected structures. Since hard formulae for the level $k$ of the existential hierarchy belong to this family, it follows that the bounded variable fragments of the full modal $\mu$-calculus form a hierarchy of strictly increasing expressive power.

  @inproceedings{BerwangerLen05,
       author = {Dietmar Berwanger and Giacomo Lenzi},
       title = {The variable hierarchy of the $\mu$-calculus is strict},
       booktitle = {STACS 2005, Proceedings of the 22nd Symposium on Theoretical Aspects of Computer Science},
       publisher = {Springer-Verlag},
       series = {LNCS},
       volume = {3404},
       year = {2005},
       pages = {97–109},
       url = {http://www.logic.rwth-aachen.de/pub/dwb/hierarchy.ps},
       task = {7},
  }
  

• A. Blumensath and S. Kreutzer. An Extension to Muchnik's Theorem. Journal of Logic and Computation, vol. 15, pp. 59–74, 2005.             
  BibTeX

  @article{BlumeKreutzer05,
       author = {Achim Blumensath and Stephan Kreutzer},
       title = {An Extension to Muchnik's Theorem},
       journal = {Journal of Logic and Computation},
       year = {2005},
       volume = {15},
       pages = {59–74},
       url = {http://www.mathematik.tu-darmstadt.de/~blumensath/Publications/Muchnik.pdf},
  }
  

• Ł. Kaiser. Confluence of Right Ground Term Rewriting Systems is Decidable. In FOSSACS 2005, Proceedings of the 8th International Conference on Foundations of Software Science and Computation Structures (V. Sassone, Ed.), vol. 3441 of LNCS. Springer-Verlag, 2005.                                 
  Abstract   BibTeX

  Term rewriting systems provide a versatile model of computation. An important property which allows to abstract from potential nondeterminism of parallel execution of the modelled program is confluence. In this paper we prove that confluence of a fairly large class of systems, namely right ground term rewriting systems, is decidable. We introduce a labelling of variables with colours and constrain substitutions according to these colours. We show how right ground rewriting systems can be reduced to simple systems with coloured variables. Such systems can be analysed using reduction-automata techniques which leads to an interesting decision procedure for confluence.

  @inproceedings{KaiserFossacs05,
       author = {Łukasz Kaiser},
       title = {Confluence of Right Ground Term Rewriting Systems is Decidable},
       booktitle = {FOSSACS 2005, Proceedings of the 8th International Conference on Foundations of Software Science and Computation Structures},
       publisher = {Springer-Verlag},
       series = {LNCS},
       editor = {Vladimiro Sassone},
       volume = {3441},
       year = {2005},
       url = {http://www.logic.rwth-aachen.de/pub/kaiser/rgtrs.pdf},
  }
  

• M. Ummels. Rational Behaviour and Strategy Construction in Infinite Multiplayer Games. Diploma thesis, RWTH Aachen, 2005.             
  BibTeX

  @misc{Ummels05,
       author = {Michael Ummels},
       title = {Rational Behaviour and Strategy Construction in Infinite Multiplayer Games},
       howpublished = {Diploma thesis, RWTH Aachen},
       year = {2005},
       url = {http://www.logic.rwth-aachen.de/~ummels/diplom.pdf},
  }
  

2004

• D. Berwanger and E. Grädel. Fixed-Point Logics and Solitaire Games. Theory of Computing Systems, vol. 37, pp. 675–694, 2004.                                 
  Abstract   BibTeX

  The model checking games associated with fixed-point logics are parity games, and it is currently not known whether the strategy problem for parity games can be solved in polynomial time. We study $\SolLFP$, a fragment of least fixed-point logic, whose evaluation games are nested soltaire games. This means that on each strongly connected component of the game, only one player can make non-trivial moves. Winning sets of nested solitaire games can be computed efficiently.

  The model checking problem for $\SolLFP$ is \sc Pspace-complete in general and \sc Ptime-complete for formulae of bounded width. On finite structures (but not on infinite ones), $\SolLFP$ is equivalent to transitive closure logic.

  We also consider the solitaire fragment of guarded fixed-point logics. Due to the restricted quantification pattern of these logics, the associated games are small and therefore admit more efficient model checking algorithms.

  @article{BerwangerGra04,
       author = {Dietmar Berwanger and Erich Grädel},
       title = {Fixed-Point Logics and Solitaire Games},
       journal = {Theory of Computing Systems},
       publisher = {Springer-Verlag},
       year = {2004},
       volume = {37},
       pages = {675–694},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/BeGr_tocs.pdf},
       task = {2,7},
  }
  

• A. Blumensath and E. Grädel. Finite Presentations of Infinite Structures: Automata and Interpretations. Theory of Computing Systems, vol. 37, pp. 641 – 674, 2004.             
  BibTeX

  @article{BlumensathGra04,
       author = {Achim Blumensath and Erich Grädel},
       title = {Finite Presentations of Infinite Structures: Automata and Interpretations},
       journal = {Theory of Computing Systems},
       publisher = {Springer-Verlag},
       year = {2004},
       volume = {37},
       pages = {641 – 674},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/BlGr_tocs.pdf},
  }
  

• A. Dawar, E. Grädel, and S. Kreutzer. Inflationary fixed points in modal logic. ACM Transations on Computational Logic, vol. 5, pp. 282 – 315, 2004.             
  BibTeX

  @article{DawarGraKre02,
       author = {Anuj Dawar and Erich Grädel and Stephan Kreutzer},
       title = {Inflationary fixed points in modal logic},
       journal = {ACM Transations on Computational Logic},
       volume = {5},
       year = {2004},
       pages = {282 – 315},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/DGK-tocl.ps},
  }
  

• A. Dawar, S. Kreutzer, and E. Grädel. Backtracking Games and Inflationary Fixed Points. In Proc. 31st International Colloquium on Automata, Languages and Programming – ICALP'04. Springer-Verlag, 2004.             
  BibTeX

  @inproceedings{DawarKreGra04,
       author = {Anuj Dawar and Stephan Kreutzer and Erich Grädel},
       title = {Backtracking Games and Inflationary Fixed Points},
       booktitle = {Proc. 31st International Colloquium on Automata, Languages and Programming – ICALP'04},
       publisher = {Springer-Verlag},
       year = {2004},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/DaGrKr-icalp04.ps},
  }
  

• E. Grädel. Positional Determinacy of Infinite Games. In Proceedings of STACS 2004: 21st Annual Symposium on Theoretical Aspects of Computer Science, vol. 2996 of LNCS, pp. 2 – 18. Springer-Verlag, 2004.             
  BibTeX

  @inproceedings{Graedel04,
       author = {Erich Grädel},
       title = {Positional Determinacy of Infinite Games},
       booktitle = {Proceedings of STACS 2004: 21st Annual Symposium on Theoretical Aspects of Computer Science},
       publisher = {Springer-Verlag},
       series = {LNCS},
       volume = {2996},
       year = {2004},
       pages = {2 – 18},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/Gr-stacs04.ps},
  }
  

• A. Nowack. Slicing Abstract State Machines. In Abstract State Machines – Advances in Theory and Practice, vol. 3052 of LNCS. Springer-Verlag, 2004.                                 
  Abstract   BibTeX

  In this work, we introduce slicing for Abstract State Machines (ASMs). The idea of this concept is analogous to the one of program slicing which is an established technique for extracting statements from a program that are relevant for its behaviour at a given point of interest. These statements form again a syntactically correct program called a slice. Previous work has focused on programming languages that differ substantially from ASMs. Although the concept of program slicing does not directly extend to ASMs, it is possible to find an analogous concept for ASMs. We present such an approach.

  In spite of the fact that a minimal slice is not computable in the general case, we identify an expressive class of ASMs for which a minimal (static) slice is computable (and prove the computability). This basic result can be extended in several ways. We present some extensions to larger classes of ASMs and other variants for the notion of slicing.

  @inproceedings{Nowack04a,
       author = {Antje Nowack},
       title = {Slicing Abstract State Machines},
       booktitle = {Abstract State Machines – Advances in Theory and Practice},
       series = {LNCS},
       volume = {3052},
       year = {2004},
       publisher = {Springer-Verlag},
       url = {http://www.logic.rwth-aachen.de/pub/nowack/asm04.ps},
  }
  

• A. Nowack. A Guarded Fragment for Abstract State Machines. In Proceedings of the ESSLLI 2004 Workshop on Guarded Fragments, 2004.                                 
  Abstract   BibTeX

  Abstract State Machines (ASMs) provide a formal method for transparent design and specification of complex dynamic systems. They combine advantages of informal and formal methods.

  Applications motivate a number of computability and decidability problems connected to ASMs. Such problems result for example from the area of verifying properties of ASMs. Their high expressive power leads rather directly to undecidability respectively uncomputability results for most interesting problems in the case of unrestricted ASMs. Consequently, it is rather natural to ask whether there exist expressive classes of ASMs for which we can prove positive decidability and computability results.

  In this work, we introduce such a class of ASMs. The idea of this class is the same as for the guarded fragment of first-order logic. We analyse the expressive power of this class and prove that it is stronger than Datalog LITE and the guarded fragment of first-order fixed point logic. Some decidability and computability results have been proven in earlier works.

  @inproceedings{Nowack04b,
       author = {Antje Nowack},
       title = {A Guarded Fragment for Abstract State Machines},
       booktitle = {Proceedings of the ESSLLI 2004 Workshop on Guarded Fragments},
       year = {2004},
       url = {http://www.logic.rwth-aachen.de/pub/nowack/GuardedASMs.ps},
  }
  

2003

• D. Berwanger. Game Logic is Strong Enough for Parity Games. Studia Logica, vol. 75(2), pp. 205–219, 2003.                                 
  Abstract   BibTeX

  We investigate the expressive power of Parikh's Game Logic interpreted in Kripke structures, and show that the syntactical alternation hierarchy of this logic is strict. This is done by encoding the winning condition for parity games of rank $n$. It follows that Game Logic is not captured by any finite level of the modal $\mu$-calculus alternation hierarchy. Moreover, we can conclude that model checking for the $\mu$-calculus is efficiently solvable iff this is possible for Game Logic.

  @article{Ber03,
       author = {Dietmar Berwanger},
       title = {Game Logic is Strong Enough for Parity Games},
       journal = {Studia Logica},
       publisher = {Kluwer},
       year = {2003},
       volume = {75},
       number = {2},
       pages = {205–219},
       note = {Special issue on Game Logic and Game Algebra edited by M. Pauly and R. Parikh},
       url = {http://journals.kluweronline.com/article.asp?PIPS=5253758},
  }
  

• D. Berwanger, E. Grädel, and S. Kreutzer. Once Upon a Time in the West. Determinacy, Complexity and Definability of Path Games. In Proceedings of the 10th International Conference on Logic for Programming and Automated Reasoning, vol. 2850 of LNCS, pp. 226–240. Springer-Verlag, 2003.                                 
  Abstract   BibTeX

  We study determinacy, definability and complexity issues of path games on finite and infinite graphs.

  Compared to the usual format of infinite games on graphs (such as Gale-Stewart games) we consider here a different variant where the players select, in each move, a path of arbitrary finite length, rather than just an edge. The outcome of a play is an infinite path, the winning condition hence is a set of infinite paths, possibly given by a formula from S1S, LTL, or first-order logic. Such games have a long tradition in descriptive set theory (in the form of Banach-Mazur games) and have recently been shown to have interesting application for planning in nondeterministic domains.

  It turns out that path games behave quite differently than classical graph games. For instance, path games with Muller conditions always admit positional winning strategies which are computable in polynomial time.

  With any logic on infinite paths (defining a winning condition) we can associate a logic on graphs, defining the winning regions of the associated path games. We explore the relationships between these logics. For instance, the winning regions of path games with an S1S-winning condition are definable in the modal mu-calculus. Further, if the winning condition is first-order (on paths), then the winning regions are definable in monadic path logic, or, for a large class of games, even in first-order logic. As a consequence, winning regions of LTL path games are definable in CTL*

  @inproceedings{BGK03,
       author = {Dietmar Berwanger and Erich Grädel and Sthephan Kreutzer},
       title = {Once Upon a Time in the West. Determinacy, Complexity and Definability of Path Games.},
       booktitle = {Proceedings of the 10th International Conference on Logic for Programming and Automated Reasoning},
       year = {2003},
       series = {LNCS},
       volume = {2850},
       pages = {226–240},
       publisher = {Springer-Verlag},
       copyright = {(c) Springer-Verlag},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/lpar03.ps},
       task = {7},
  }
  

• A. Blumensath. Structures of Bounded Partition Width. PhD thesis, RWTH Aachen, 2003.             
  BibTeX

  @phdthesis{Blumensath03,
       author = {A. Blumensath},
       title = {Structures of Bounded Partition Width},
       year = {2003},
       school = {RWTH Aachen},
       address = {Aachen},
       type = {Ph.D. Thesis},
       url = {http://www.logic.rwth-aachen.de/pub/blume/Partition.ps.gz},
  }
  

• E. Grädel. Decidable fragments of first-order and fixed-point logic. From prefix-vocabulary classes to guarded logics. In Proceedings of Kalmár Workshop on Logic and Computer Science, Szeged, 2003.             
  BibTeX

  @inproceedings{Graedel03a,
       author = {E. Grädel},
       title = {Decidable fragments of first-order and fixed-point logic. From prefix-vocabulary classes to guarded logics.},
       booktitle = {Proceedings of Kalmár Workshop on Logic and Computer Science, Szeged},
       year = {2003},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/Gr-kalmar03.ps},
  }
  

• E. Grädel and S. Kreutzer. Will Deflation Lead to Depletion? On Non-Monotone Fixed Point Inductions. In Proceedings of 18th IEEE Symposium on Logic in Computer Science (LICS), pp. 158 – 167, 2003.             
  BibTeX

  @inproceedings{GraedelKr03,
       author = {Erich Grädel and Stephan Kreutzer},
       title = {Will Deflation Lead to Depletion? On Non-Monotone Fixed Point Inductions.},
       booktitle = {Proceedings of 18th IEEE Symposium on Logic in Computer Science (LICS)},
       year = {2003},
       pages = {158 – 167},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/GrKr-lics03.ps},
  }
  

• E. Grädel and A. Nowack. Quantum Computing and Abstract State Machines. In Abstract State Machines – Advances in Theory and Applications, vol. 2589 of LNCS, pp. 309 – 323. Springer-Verlag, 2003.             
  BibTeX

  @inproceedings{GraedelNo03,
       author = {Erich Grädel and Antje Nowack},
       title = {Quantum Computing and Abstract State Machines},
       booktitle = {Abstract State Machines – Advances in Theory and Applications},
       series = {LNCS},
       volume = {2589},
       pages = {309 – 323},
       year = {2003},
       publisher = {Springer-Verlag},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/GrNo-asm03.ps},
  }
  

• S. Kreutzer. Pure and Applied Fixed-Point Logics. In Ausgezeichnete Informatikdissertationen 2002 (D. Wagner et al., Eds.), vol. D-3 of Lecture Notes in Informatics – Dissertations, pp. 59–68. German Informatics Society, 2003.             
  BibTeX

  @incollection{Kre03d,
       author = {Stephan Kreutzer},
       title = {Pure and Applied Fixed-Point Logics},
       booktitle = {Ausgezeichnete Informatikdissertationen 2002},
       pages = {59–68},
       publisher = {German Informatics Society},
       year = {2003},
       editor = {Dorothea Wagner and Others},
       volume = {D-3},
       series = {Lecture Notes in Informatics – Dissertations},
  }
  

• A. Nowack. Deciding the Verification Problem for Abstract State Machines. In Abstract State Machines – Advances in Theory and Applications, vol. 2589 of LNCS. Springer-Verlag, 2003.                                 
  Abstract   BibTeX

  We study the decdability of general verification problems for ASMs. This corresponds to the question whether all computations of an ASM satisfy a property (usually expressed in some temporal logic). Because of undecidability in the general case, one has to identify classes of ASMs and classes of properties in order to receive positive decidability results. One idea for this could be to put simple restrictions on the ASMs as forbidding certain advanced constructs. But it turns out that this does not help much. Additionally, the restrictions in those cases are very strong. Consequently, one has to look for others. Such restrictions may result from techniques which are intended to be used in the proofs of decidability. One proof technique is the reduction to a decidable reasoning problem in logic. M. Spielmann has applied it to receive some positive decidability results.

  In this paper, we identify further classes of ASMs and classes of properties for which the general verification problem is decidable. Each proof is a reduction to the satisfiability problem of a fragment of linear temporal first-order logic which has respectively been proved to be decidable by I. Hodkinson, F. Wolter and M. Zakharyaschev.

  @inproceedings{Nowack03,
       author = {Antje Nowack},
       title = {Deciding the Verification Problem for Abstract State Machines},
       booktitle = {Abstract State Machines – Advances in Theory and Applications},
       series = {LNCS},
       volume = {2589},
       year = {2003},
       publisher = {Springer-Verlag},
       url = {http://www.logic.rwth-aachen.de/pub/nowack/asm03.ps},
  }
  

2002

• D. Berwanger and A. Blumensath. Automata for Guarded Fixed Point Logics. In Automata, Logics, and Infinite Games (E. Grädel, W. Thomas, and T. Wilke, Eds.), LNCS, pp. 343-355. Springer Verlag, 2002.             
  BibTeX

  @incollection{BerwangerBl02,
       author = {Dietmar Berwanger and Achim Blumensath},
       title = {Automata for Guarded Fixed Point Logics},
       booktitle = {Automata, Logics, and Infinite Games},
       pages = {343-355},
       publisher = {Springer Verlag},
       year = {2002},
       editor = {E. Grädel and W. Thomas and T. Wilke},
       number = {2500},
       series = {LNCS},
       chapter = {19},
       url = {http://www.logic.rwth-aachen.de/pub/dwb/guarded.ps},
  }
  

• D. Berwanger and A. Blumensath. The Monadic Theory of Tree-like Structures. In Automata, Logics, and Infinite Games (E. Grädel, W. Thomas, and T. Wilke, Eds.), LNCS, pp. 285-301. Springer Verlag, 2002.             
  BibTeX

  @incollection{BlumensathBe02,
       author = {Dietmar Berwanger and Achim Blumensath},
       title = {The Monadic Theory of Tree-like Structures},
       booktitle = {Automata, Logics, and Infinite Games},
       pages = {285-301},
       publisher = {Springer Verlag},
       year = {2002},
       editor = {E. Grädel and W. Thomas and T. Wilke},
       number = {2500},
       series = {LNCS},
       chapter = {16},
       url = {http://www.logic.rwth-aachen.de/pub/dwb/muchnik.ps},
  }
  

• D. Berwanger and E. Grädel. Fixed point formulae and solitaire games. In Proceedings of the 2nd International Workshop on Complexity in Automated Deduction, CiAD 2002, 2002.                                 
  Abstract   BibTeX

  The model checking games associated with fixed point logics are parity games, and it is currently not known whether the strategy problem for parity games can be solved in polynomial time. We study , a fragment of least fixed point logic, whose model checking games are nested soltaire games. This means that on each strongly connected component of the game, only one player can make non-trivial moves. Winning sets of nested solitaire games can be efficiently computed. The model checking problem for is Pspace-complete in general and Ptime-complete for formulae of bounded width. On finite structures (but not on infinite ones), is equivalent to transitive closure logic.

  @inproceedings{BerwangerGra02,
       author = {Dietmar Berwanger and Erich Grädel},
       title = {Fixed point formulae and solitaire games},
       booktitle = {Proceedings of the 2nd International Workshop on Complexity in Automated Deduction, CiAD 2002},
       year = {2002},
       url = {http://www.logic.rwth-aachen.de/pub/dwb/ciad02.ps},
       task = {7},
  }
  

• D. Berwanger, E. Grädel, and G. Lenzi. On the variable hierarchy of the modal mu-calculus. In Computer Science Logic, CSL 2002 (J. Bradfield, Ed.), vol. 2471 of LNCS, pp. 352–366. Springer-Verlag, 2002.                                 
  Abstract   BibTeX

  Most of the logics commonly used in verification, such as CTL, LTL, CTL*, PDL, etc. can in fact be embedded into the two-variable fragment of the mu-calculus. It is also known that the two-variable fragment can express properties that occur at arbitrarily high levels of the alternation hierarchy. However, it is an open problem whether the variable hierarchy is strict. Here we study this problem with a game-based approach and establish the strictness of the hierarchy for the case of existential (i.e., Box-free) formulae. It is known that these characterize precisely the L_\mu-definable properties that are closed under extensions. We also relate the strictness of the variable hierarchy to the question whether the finite variable fragments satisfy the existential preservation theorem.

  @inproceedings{BerwangerGraLen02,
       author = {Dietmar Berwanger and Erich Grädel and Giacomo Lenzi},
       title = {On the variable hierarchy of the modal mu-calculus},
       booktitle = {Computer Science Logic, CSL 2002},
       editor = {Julian Bradfield},
       year = {2002},
       series = {LNCS},
       volume = {2471},
       pages = {352–366},
       publisher = {Springer-Verlag},
       copyright = {(c) Springer-Verlag},
       url = {http://www.logic.rwth-aachen.de/pub/dwb/csl02.ps},
  }
  

• A. Blumensath. Axiomatising Tree-interpretable Structures. In Proceedings of 19th International Symposium on Theoretical Aspects of Computer Science, vol. 2285 of LNCS, pp. 596–607. Springer-Verlag, 2002.                                 
  Abstract   BibTeX

  Generalising the notion of a prefix-recognisable graph to arbitrary relational structures we introduce the class of tree-interpretable structures. We prove that every tree-interpretable structure is finitely axiomatisable in guarded second-order logic with cardinality quantifiers.

  @inproceedings{Bl02,
       author = {A. Blumensath},
       title = {Axiomatising Tree-interpretable Structures},
       booktitle = {Proceedings of 19th International Symposium on Theoretical Aspects of Computer Science},
       year = {2002},
       series = {LNCS},
       publisher = {Springer-Verlag},
       copyright = {(c) Springer-Verlag},
       volume = {2285},
       pages = {596–607},
       url = {http://www.logic.rwth-aachen.de/pub/blume/stacs02.ps.gz},
  }
  

• A. Blumensath and E. Grädel. Finite Presentations of Infinite Structures. In Proceedings of the 2nd International Workshop on Complexity in Automated Deduction, CiAD 2002, 2002.                                 
  Abstract   BibTeX

  We study definability problems and algorithmic issues for infinite structures that are finitely presented. After a brief overview over different classes of finitely presentable structures, we focus on structures presented by automata or by model-theoretic interpretations. These two ways of presenting a structure are related. Indeed, a structure is automatic if, and only if, it is first-order interpretable in an appropriate expansion of Presburger arithmetic or, equivalently, in the infinite binary tree with prefix order and equal length predicate. Similar results hold for $\omega$-automatic structures and appropriate expansions of the real ordered group. We also discuss the relationship to automatic groups. The model checking problem for $\FO(\exists^\omega)$, first-order logic extended by the quantifier ``there are infinitely many'', is proved to be decidable for automatic and $\omega$-automatic structures. Further, the complexity for various fragments of first-order logic is determined. On the other hand, several important properties not expressible in $\FO$, such as isomorphism or connectedness, turn out to be undecidable for automatic structures. Finally, we investigate methods for proving that a structure does not admit an automatic presentation, and we establish that the class of automatic structures is closed under Feferman-Vaught like products

  @inproceedings{BlumensathGra02,
       author = {Achim Blumensath and Erich Grädel},
       title = {Finite Presentations of Infinite Structures},
       booktitle = {Proceedings of the 2nd International Workshop on Complexity in Automated Deduction, CiAD 2002},
       year = {2002},
       note = {Submitted to ACM Theory of Computing Systems},
       url = {http://www.logic.rwth-aachen.de/pub/blume/tocs-2002-ciad.ps},
  }
  

• A. Dawar and S. Kreutzer. Generalising Automaticity to Modal Properties of Finite Structures. In Foundations of Software Technology and Theoretical Computer Science, 2002.                                 
  Abstract   BibTeX

  We introduce a complexity measure of modal properties of finite structures which generalises the automaticity of languages. It is based on graph-automata like devices called labelling systems. We define a measure of the size of a structure that we call rank, and show that any modal property of structures can be approximated up to any fixed rank n by a labelling system. The function that takes n to the size of the smallest labelling system doing this is called the labelling index of the property. We demonstrate that this is a useful and fine-grained measure of complexity and show that it is especially well suited to characterise the expressive power of modal fixed-point logics. From this we derive several separation results of modal and non-modal fixed-point logics, some of which are already known whereas others are new.

  @inproceedings{KreutzerDaw02,
       author = {Anuj Dawar and Stephan Kreutzer},
       title = {Generalising Automaticity to Modal Properties of Finite Structures},
       booktitle = {Foundations of Software Technology and Theoretical Computer Science},
       year = {2002},
       url = {http://www.logic.rwth-aachen.de/pub/kreutzer/fsttcs.ps},
  }
  

• G. Gottlob, E. Grädel, and H. Veith. Datalog LITE: A deductive query language with linear time model checking. ACM Transactions on Computational Logic, vol. 3(1), pp. 1–35, 2002.             
  BibTeX

  @article{GoGrVe99,
       author = {G. Gottlob and E. Grädel and H. Veith},
       title = {Datalog LITE: A deductive query language with linear time model checking},
       journal = {ACM Transactions on Computational Logic},
       year = {2002},
       volume = {3},
       number = {1},
       pages = {1–35},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/GoGrVe-tocl02.ps},
  }
  

• E. Grädel. Guarded fixed point logic and the monadic theory of trees. Theoretical Computer Science, vol. 288, pp. 129–152, 2002.             
  BibTeX

  @article{Gr02,
       author = {E. Grädel},
       title = {Guarded fixed point logic and the monadic theory of trees},
       journal = {Theoretical Computer Science},
       volume = {288},
       year = {2002},
       pages = {129–152},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/Gr-tcs01.ps},
  }
  

• E. Grädel. Model Checking Games. In Proceedings of WOLLIC 02, vol. 67 of Electronic Notes in Theoretical Computer Science. Elsevier, 2002.                                 
  Abstract   BibTeX

  We survey evaluation algorithms for first-order logic and least fixed point logics, and discuss their algorithmic complexity

  @inproceedings{GrWollic02,
       author = {E. Grädel},
       title = {Model Checking Games},
       booktitle = {Proceedings of WOLLIC 02},
       series = {Electronic Notes in Theoretical Computer Science},
       publisher = {Elsevier},
       volume = {67},
       year = {2002},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/Gr-wollic02.ps},
  }
  

• E. Grädel, C. Hirsch, and M. Otto. Back and Forth Between Guarded and Modal Logics. ACM Transactions on Computational Logics, vol. 3(3), pp. 418 – 463, 2002.                                 
  Abstract   BibTeX

  Guarded fixed-point logic $\mu$GF extends the guarded fragment by means of least and greatest fixed points, and thus plays the same role within the domain of guarded logics as the modal $\mu$-calculus plays within the modal domain. We provide a semantic characterization of $\mu$GF within an appropriate fragment of second-order logic, in terms of invariance under guarded bisimulation. The corresponding characterization of the modal $\mu$-calculus, due to Janin and Walukiewicz, is lifted from the modal to the guarded domain by means of model theoretic translations. Guarded second-order logic, the fragment of second-order logic which is introduced in the context of our characterization theorem, captures a natural and robust level of expressiveness with several equivalent characterizations. For a wide range of issues in guarded logics it may take up a role similar to that of monadic second-order in relation to modal logics. At the more general methodological level, the translations between the guarded and modal domains make the intuitive analogy between guarded and modal logics available as a tool in the further analysis of the model theory of guarded logics.

  @article{GrHiOt00a,
       author = {E. Grädel and C. Hirsch and M. Otto},
       title = {Back and Forth Between Guarded and Modal Logics},
       journal = {ACM Transactions on Computational Logics},
       pages = {418 – 463},
       volume = {3},
       number = {3},
       year = {2002},
       note = {See also: conference version \citeGrHiOt00},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/GrHiOt-tocl02.ps},
  }
  

• E. Grädel, W. Thomas, and T. Wilke (Eds.). Automata, Logics, and Infinite Games. Springer-Verlag, 2002.             
  BibTeX

  @book{GraedelThoWil02,
       editor = {E. Grädel and W. Thomas and T. Wilke},
       title = {Automata, Logics, and Infinite Games},
       publisher = {Springer-Verlag},
       year = {2002},
       series = {Lecture Notes in Compter Science},
       number = {2500},
       url = {http://www.logic.rwth-aachen.de/Books/},
  }
  

• C. Hirsch. Guarded Logics: Algorithms and Bisimulation. PhD thesis, RWTH Aachen, 2002.             
  BibTeX

  @phdthesis{HirschThesis,
       author = {Colin Hirsch},
       title = {Guarded Logics: Algorithms and Bisimulation},
       school = {RWTH Aachen},
       year = {2002},
       url = {http://www.logic.rwth-aachen.de/pub/hirsch/hirsch.pdf},
  }
  

• S. Kreutzer. Expressive Equivalence of Least and Inflationary Fixed-Point Logic. In Proceedings of the 17th IEEE Symp. on Logic in Computer Science (LICS), 2002.                                 
  Abstract   BibTeX

  We study the relationship between least and inflationary fixed-point logic. By results of Gurevich and Shelah from 1986, it has been known that on finite structures both logics have the same expressive power. On infinite structures however, the question whether there is a formula in $\IFP$ not equivalent to any $\LFP$-formula was still open. In this paper, we settle the question by showing that both logics are equally expressive on arbitrary structures. The proof will also establish the strictness of the nesting-depth hierarchy for $\IFP$ on some infinite structures. Finally, we show that the alternation hierarchy for $\IFP$ collapses to the first level on all structures, i.e. the complement of an inflationary fixed-point is an inflationary fixed-point itself.

  @inproceedings{Kreutzer02,
       author = {S. Kreutzer},
       title = {Expressive Equivalence of Least and Inflationary Fixed-Point Logic},
       booktitle = {Proceedings of the 17th IEEE Symp. on Logic in Computer Science (LICS)},
       year = {2002},
       url = {http://www.logic.rwth-aachen.de/pub/kreutzer/ifp.ps},
  }
  

• S. Kreutzer. Partial Fixed-Point Logic on Infinite Structures. In Annual Conference of the European Association for Computer Science Logic (CSL), vol. 2471 of Lecture Notes in Computer Science (LNCS). Springer, 2002.                                 
  Abstract   BibTeX

  We consider an alternative semantics for partial fixed-point logic (PFP) To define the fixed point of a formula in this semantics, the sequence of stages induced by the formula is considered. As soon as this sequence becomes cyclic, the set of elements contained in every stage of the cycle is taken as the fixed point. It is shown that on finite structures, this fixed-point semantics and the standard semantics for PFP as considered in finite model theory are equivalent, although arguably the formalisation of properties might even become simpler and more intuitive. Contrary to the standard PFP semantics which is only defined on finite structures the new semantics generalises easily to infinite structures and transfinite inductions. In this generality we compare – in terms of expressive power – partial with other known fixed-point logics. The main result of the paper is that on arbitrary structures, PFP is strictly more expressive than inflationary fixed-point logic (IFP). A separation of these logics on finite structures would prove PTIME different from PSPACE.

  @inproceedings{Kreutzer02b,
       author = {S. Kreutzer},
       title = {Partial Fixed-Point Logic on Infinite Structures},
       booktitle = {Annual Conference of the European Association for Computer Science Logic (CSL)},
       year = {2002},
       volume = {2471},
       series = {Lecture Notes in Computer Science (LNCS)},
       publisher = {Springer},
  }
  

• S. Kreutzer. Pure and Applied Fixed-Point Logics. PhD thesis, RWTH Aachen, 2002.             
  BibTeX

  @phdthesis{KreutzerThesis,
       author = {Stephan Kreutzer},
       title = {Pure and Applied Fixed-Point Logics},
       school = {RWTH Aachen},
       year = {2002},
       url = {http://www.logic.rwth-aachen.de/pub/kreutzer/kreutzer.pdf},
  }
  

• E. Rosen. Some aspects of model theory and finite structures. Bulletin of Symbolic Logic, vol. 8(3), pp. 380 – 403, 2002.             
  BibTeX

  @article{Rosen02,
       author = {Eric Rosen},
       title = {Some aspects of model theory and finite structures},
       journal = {Bulletin of Symbolic Logic},
       year = {2002},
       volume = {8},
       number = {3},
       pages = {380 – 403},
       url = {http://www.logic.rwth-aachen.de/pub/rosen/Rosen02.ps},
  }
  

2001

• D. Berwanger and E. Grädel. Games and Model Checking for Guarded Logics. In Proceedings of the 8th International Conference on Logic for Programming and Automated Reasoning, LPAR 2001, Havana (R. Nieuwenhuis and A. Voronkov, Eds.), vol. 2250 of LNCS. Springer-Verlag, 2001.                                 
  Abstract   BibTeX

  We investigate the model checking problems for guarded first-order and fixed point logics by reducing them to parity games. This approach is known to provide good results for the modal $\mu$-calculus and is very closely related to automata-based methods. To obtain good results also for guarded logics, optimized constructions of games have to be provided.

  Further, we study the structure of parity games, isolate èasy' cases that admit efficient algorithmic solutions, and determine their relationship to specific fragments of guarded fixed point logics.

  @inproceedings{BeGr01,
       author = {D. Berwanger and E. Grädel},
       title = {Games and Model Checking for Guarded Logics},
       booktitle = {Proceedings of the 8th International Conference on Logic for Programming and Automated Reasoning, LPAR 2001, Havana},
       editor = {R. Nieuwenhuis and A. Voronkov},
       year = {2001},
       series = {LNCS},
       volume = {2250},
       publisher = {Springer-Verlag},
       copyright = {(c) Springer-Verlag},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/lpar.ps},
  }
  

• D. Berwanger. Game Logic is Strong Enough for Parity Games. In Proceedings of the ESSLLI 2001 Workshop on Logic and Games (M. Pauly and G. Sandu, Eds.), Helsinki, 2001.                                 
  Abstract   BibTeX

  This paper is concerned with the expressive power of Parikh's Game Logic interpreted in Kripke structures. We show that the syntactical alternation hierarchy of this logic is strict, by expressing the winning condition for parity games with $n$ priorities. Moreover, it follows that Game Logic is not captured by any finite level of the $\mu$-calculus alternation hierarchy. We can further conclude that model checking for the $\mu$-calculus is efficiently solvable iff this is possible for Game Logic.

  @inproceedings{Ber01,
       author = {D. Berwanger},
       title = {Game Logic is Strong Enough for Parity Games},
       booktitle = {Proceedings of the ESSLLI 2001 Workshop on Logic and Games},
       editor = {M. Pauly and G. Sandu},
       year = {2001},
       address = {Helsinki},
       note = {Conference version of \citeBer03},
       url = {http://www.logic.rwth-aachen.de/pub/dwb/helsinki.ps},
  }
  

• A. Blumensath. Prefix-Recognisable Graphs and Monadic Second-Order Logic. Technical Report. RWTH Aachen, 2001.                                 
  Abstract   BibTeX

  We present several characterisations of the class of prefix-recognisable graphs including representations via graph-grammars and MSO-interpretations. The former implies that prefix-recognisable graphs have bounded clique-width; the latter is used to extend this class to arbitrary relational structures. We prove that the prefix-recognisable groups are exactly the context-free groups. Finally, we develop methods to prove that certain structures are not prefix-recognisable and apply them to well-ordered structures.

  @techreport{Bl01,
       author = {Achim Blumensath},
       title = {Prefix-Recognisable Graphs and Monadic Second-Order Logic},
       institution = {RWTH Aachen},
       year = {2001},
       number = {AIB-06-2001},
       month = {May},
       url = {http://www.logic.rwth-aachen.de/pub/blume/aib-2001-06.ps.gz},
  }
  

• A. Dawar, E. Grädel, and S. Kreutzer. Inflationary Fixed Points in Modal Logic. In Proceedings of 15th Annual Conference of the European Association for Computer Science Logic CSL 2001, LNCS. Springer-Verlag, 2001.                                 
  Abstract   BibTeX

  We consider an extension of modal logic with an operator for constructing inflationary fixed points, just as the modal $\mu$-calculus extends basic modal logic with an operator for least fixed points. Least and inflationary fixed point operators have been studied and compared in other contexts, particularly in finite model theory, where it is known that the logics IFP and LFP that result from adding such fixed point operators to first order logic have equal expressive power. As we show, the situation in modal logic is quite different, as the modal iteration calculus ($\MIC$) we introduce has much greater expressive power than the $\mu$-calculus. Greater expressive power comes at a cost: the calculus is algorithmically much less manageable.

  @inproceedings{DGK01,
       author = {A. Dawar and E. Grädel and S. Kreutzer},
       title = {Inflationary Fixed Points in Modal Logic},
       booktitle = {Proceedings of 15th Annual Conference of the European Association for Computer Science Logic CSL 2001},
       year = {2001},
       series = {LNCS},
       publisher = {Springer-Verlag},
       copyright = {(c) Springer-Verlag},
       url = {http://www.logic.rwth-aachen.de/pub/kreutzer/csl01.ps},
  }
  

• J. Duparc. Wadge hierarchy and Veblen hierarchy. Part I: Borel sets of finite rank. Journal of Symbolic Logic, vol. 66(1), pp. 56–86, 2001.                                 
  Abstract   BibTeX

  We consider Borel sets of finite rank $A\subseteq\Lambda^\omega$ where cardinality of $\Lambda$ is less than some uncountable regular cardinal $\kappa$. We obtain a ''normal form'' of $A$, by finding a Borel set $\Omega$, such that $A$ and $\Omega$ continuously reduce to each other. In more technical terms: we define simple Borel operations which are homomorphic to ordinal sum, to multiplication by a countable ordinal, and to ordinal exponentiation of base $\kappa$, under the map which sends every Borel set $A$ of finite rank to its Wadge degree.

  @article{JDjsl1,
       author = {J. Duparc},
       title = {Wadge hierarchy and Veblen hierarchy. Part I: Borel sets of finite rank},
       journal = {Journal of Symbolic Logic},
       year = {2001},
       volume = {66},
       number = {1},
       pages = {56–86},
  }
  

• J. Duparc. Wadge hierarchy and Veblen hierarchy. Part II: Borel sets of infinite rank. Submitted to Journal of Symbolic Logic, 2001.                                 
  Abstract   BibTeX

  We consider Borel sets of the form $A\subseteq\Lambda^\omega$ (with usual topology) where cardinality of $\Lambda$ is less than some uncountable regular cardinal $\kappa$. We obtain a ''normal form'' of $A$, by finding a Borel set $\Omega(\alpha)$ such that $A$ and $\Omega(\alpha)$ continuously reduce to each other. We do so by defining Borel operations which are homomorphic to the $\kappa$ first Veblen ordinal functions of base $\kappa$ required to compute the Wadge degree of the set $A$: the ordinal $\alpha$.

  @article{JDjsl2,
       author = {J. Duparc},
       title = {Wadge hierarchy and Veblen hierarchy. Part II: Borel sets of infinite rank},
       journal = {Submitted to Journal of Symbolic Logic},
       year = {2001},
       url = {http://www.logic.rwth-aachen.de/pub/duparc/jsl2.ps},
  }
  

• J. Duparc. The Steel Hierarchy of Ordinal Valued Borel Mappings. Submitted to Journal of Symbolic Logic, 2001.                                 
  Abstract   BibTeX

  Given well ordered countable sets of the form $\Lambda_\phi$, we consider Borel mappings from $\Lambda_\phi^\omega$ with countable image inside the ordinals. The ordinals and $\Lambda_\phi^\omega$ are respectively equipped with the discrete topology and the product of the discrete topology on $\Lambda_\phi$. The Steel well-ordering on such mappings is defined by $\phi\leq_S\psi$ iff there exists a continuous function $f$ such that $\phi(x)\leq\psi\circ\psi(x)$ holds for any $x\in\Lambda_\phi^\omega$. It induces a hierachy of mappings which we give a complete description of. We provide, for each ordinal $\alpha$, a mapping $\hbox$\mathbb{T$}(\alpha)$ whose rank is precisely $\alpha$ in this hierarchy and we also compute the height of the hierarchy restricted to mappings with image bounded by $\alpha$. These mappings being viewed as partitions of the reals, there is, in most cases, a unique distinguished element of the partition. We analyze the relation between its topological complexity and the rank of the mapping in this hierarchy.

  @article{JDjsl3,
       author = {J. Duparc},
       title = {The Steel Hierarchy of Ordinal Valued Borel Mappings},
       journal = {Submitted to Journal of Symbolic Logic},
       year = {2001},
       url = {http://www.logic.rwth-aachen.de/pub/duparc/jsl3.ps},
  }
  

• J. Duparc. Wadge degrees of Louveau's (Wadge) classes. 2001.                                 
  Abstract   BibTeX

  For each Wadge class of Borel sets of reals, as described in Louveau's works, we produce a set that is complete for this class, and is canonical in the sense it is defined by operations on sets that are the set theoretic counterparts of natural operations on ordinals. This allow to (inductively) compute the Wadge degree of all Louveau's (Wadge) classes

  @unpublished{JDns1,
       author = {J. Duparc},
       title = {Wadge degrees of Louveau's (Wadge) classes},
       note = {To be extended, then submitted},
       year = {2001},
       url = {http://www.logic.rwth-aachen.de/pub/duparc/ns1.ps},
  }
  

• J. Duparc. A coarsification of the Wagner Hierarchy. Submitted to Theoretical Computer Science, 2001.                                 
  Abstract   BibTeX

  In 1979, Klaus W. Wagner introduced a hierarchy on $\omega$-regular sets that has length $\omega^\omega$. It is the one induced by the ordering on Deterministic Automata: $\cal A\leq \cal B$ iff the set accepted by $\cal A$ is the inverse image of the set accepted by $\cal B$ by a continuous function. Lately, Jean-Eric Pin conjectured that there might be a coarser hierarchy with length $\omega$ and that it could be given by the same ordering on DA except that continuous is replaced by a slightly weaker notion 2-continuous. We provide a positive answer to this conjecture and give a description of this new hierarchy.

  @article{JDtcs3,
       author = {J. Duparc},
       title = {A coarsification of the Wagner Hierarchy},
       journal = {Submitted to Theoretical Computer Science},
       year = {2001},
       url = {http://www.logic.rwth-aachen.de/pub/duparc/tcs3.ps},
  }
  

• O. Finkel, J. Duparc, and J. Ressayre. Computer Science and the fine structure of Borel sets. Theoretical Computer Science, pp. 85–105, 2001.                                 
  Abstract   BibTeX

  Wadge defined a natural refinement of the Borel hierarchy, now called the Wadge hierarchy WH. The fundamental properties of WH follow from results of Kuratowski, Martin,Wadge and Louveau. We give a transparent restatement and proof of Wadge's main theorem. Our method is new for it yields a wide and unexpected extension: from Borel sets of reals to a class of natural but non Borel sets of infinite sequences. Wadge's theorem is quite uneffective and our generalization clearly worse in this respect. Yet paradoxically our method is appropriate to effectivize this whole theory in the context discussed below.

  Wagner defined on Büchi automata (accepting words of length $\omega$) a hierarchy and proved for it an effective analog of Wadge's results. We extend Wagner's results to more general kinds of Automata: Counters, Push Down Automata and Büchi Automata reading transfinite words. The notions and methods developed in \refone\ are quite useful for this extension. And we start to use them in order to look for extensions of the fundamental effective determinacy results of Büchi-Landweber, Rabin; and of Courcelle-Walukiewicz.

  @article{JDtcs1,
       author = {O. Finkel and J. Duparc and J-P. Ressayre},
       title = {Computer Science and the fine structure of Borel sets},
       journal = {Theoretical Computer Science},
       year = {2001},
       number = {257},
       pages = {85–105},
  }
  

• E. Grädel. Why are modal logics so robustly decidable?. In Current Trends in Theoretical Computer Science. Entering the 21st Century (G. Paun, G. Rozenberg, and A. Salomaa, Eds.), pp. 393–408. World Scientific, 2001.             
  BibTeX

  @incollection{Gr01,
       author = {E. Grädel},
       title = {Why are modal logics so robustly decidable?},
       booktitle = {Current Trends in Theoretical Computer Science. Entering the 21st Century},
       editor = {G. Paun and G. Rozenberg and A. Salomaa},
       pages = {393–408},
       publisher = {World Scientific},
       year = {2001},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/Gr-trends01.ps},
  }
  

• C. Hirsch and R. Fleischer. Graph Drawings and Its Applications. In Drawing Graphs – Methods and Models (M. Kaufmann and D. Wagner, Eds.), LNCS, pp. 1–22. Springer-Verlag, 2001.             
  BibTeX

  @incollection{HiFl01,
       author = {C. Hirsch and R. Fleischer},
       title = {Graph Drawings and Its Applications},
       booktitle = {Drawing Graphs – Methods and Models},
       editor = {M. Kaufmann and D. Wagner},
       publisher = {Springer-Verlag},
       series = {LNCS},
       pages = {1–22},
       chapter = {1},
       year = {2001},
       copyright = {(c) Springer-Verlag},
  }
  

• S. Kreutzer. Query Languages for Constraint Databases: First-Order Logic, Fixed-Points, and Convex Hulls. In Proceedings of the 8th International Conference on Database Theory (ICDT), vol. 1973 of LNCS, pp. 248–262. Springer-Verlag, 2001.                                 
  Abstract   BibTeX

  We define various extensions of first-order logic on linear as well as polynomial constraint databases. First, we extend first-order logic by a convex closure operator and show this logic, FO(conv), to be closed and to have PTIME data-complexity. We also show that a weak form of multiplication is definable in this language and prove the equivalence between this language and the multiplication part of PFOL. We then extend FO(conmv) by fixed-point operators to get a query languages expressive enough to capture PTIME. In the last part of the paper we lift the results to polynomial constraint databases.

  @inproceedings{Kreutzer01,
       author = {S. Kreutzer},
       title = {Query Languages for Constraint Databases: First-Order Logic, Fixed-Points, and Convex Hulls},
       booktitle = {Proceedings of the 8th International Conference on Database Theory (ICDT)},
       year = {2001},
       series = {LNCS},
       publisher = {Springer-Verlag},
       copyright = {(c) Springer-Verlag},
       pages = {248–262},
       volume = {1973},
       url = {http://www.logic.rwth-aachen.de/pub/kreutzer/icdt2001.ps},
  }
  

• S. Kreutzer. Operational Semantics for Fixed-Point Logics on Constraint Databases. In Proceedings of the 8th International Conference on Logic for Programming and Automated Reasoning, LPAR 2001, Havana, vol. 2250 of LNCS, pp. 465–479. Springer-Verlag, 2001.                                 
  Abstract   BibTeX

  In this paper we compare the expressive power of various fixed-point logics on linear or dense order constraint databases. This comparison is not done on absolute terms, i.e. by comparing their expressive power for arbitrary queries, rather for definability of partially recursive queries. The motivation for choosing this benchmark comes from fixed-point logics as query languages for constraint databases. Here, non-recursive queries are of no practical interest. It is shown that for linear constraint databases already transitive closure logic is expressive enough to define all partially recursive queries, i.e., transitive-closure logic is expressively complete for this class of databases. It follows that transitive-closure, least, and stratified fixed-point logic are equivalent with respect to this benchmark.

  @inproceedings{Kreutzer01b,
       author = {S. Kreutzer},
       title = {Operational Semantics for Fixed-Point Logics on Constraint Databases},
       booktitle = {Proceedings of the 8th International Conference on Logic for Programming and Automated Reasoning, LPAR 2001, Havana},
       year = {2001},
       series = {LNCS},
       volume = {2250},
       pages = {465–479},
       publisher = {Springer-Verlag},
       copyright = {(c) Springer-Verlag},
       url = {http://www.logic.rwth-aachen.de/pub/kreutzer/lpar01.ps},
  }
  

2000

• D. Berwanger. Games and Model Checking for Guarded Logics. Diploma thesis, RWTH-Aachen, 2000.             
  BibTeX

  @misc{Ber00,
       author = {D. Berwanger},
       title = {Games and Model Checking for Guarded Logics},
       howpublished = {Diploma thesis, RWTH-Aachen},
       year = {2000},
       url = {http://www.logic.rwth-aachen.de/pub/dwb/ber00.ps.gz},
  }
  

• A. Blumensath. Bounded Arithmetic and Descriptive Complexity. In Proceedings of 14th Annual Conference of the European Association for Computer Science Logic CSL 2000, vol. 1862 of LNCS, pp. 232–246. Springer-Verlag, 2000.                                 
  Abstract   BibTeX

  We study definability of languages in arithmetic and the free monoid by bounded versions of fixed-point and transitive-closure logics. In particular we give logical characterisations of complexity classes C by showing that a language belongs to C if and only if it is definable in either arithmetic or the free monoid by a formula of a certain logic. We investigate in which cases the bounds of fixed-point operators may be omitted. Finally, a general translation of results from descriptive complexity to the approach described in this paper is presented.

  @inproceedings{Bl00,
       author = {A. Blumensath},
       title = {Bounded Arithmetic and Descriptive Complexity},
       booktitle = {Proceedings of 14th Annual Conference of the European Association for Computer Science Logic CSL 2000},
       year = {2000},
       series = {LNCS},
       publisher = {Springer-Verlag},
       copyright = {(c) Springer-Verlag},
       volume = {1862},
       pages = {232–246},
       url = {http://www.logic.rwth-aachen.de/pub/blume/csl00.ps.gz},
  }
  

• A. Blumensath and E. Grädel. Automatic Structures. In Proceedings of 15th IEEE Symposium on Logic in Computer Science LICS 2000, pp. 51–62, 2000.                                 
  Abstract   BibTeX

  We study definability and complexity issues for automatic and omega-automatic structures. These are, in general, infinite structures but they can be finitely presented by a collection of automata. Moreover, they admit effective (in fact automatic) evaluation of all first-order queries. Therefore, automatic structures provide an interesting framework for extending many algorithmic and logical methods from finite structures to infinite ones. \par We explain the notion of (omega-)automatic structures, give examples, and discuss the relationship to automatic groups. We determine the complexity of model checking and query evaluation on automatic structures for fragments of first-order logic. Further, we study closure properties and definability issues on automatic structures and present a technique for proving that a structure is not automatic. We give model-theoretic characterisations for automatic structures via interpretations. Finally we discuss the composition theory of automatic structures and prove that they are closed under finitary Feferman-Vaught-like products.

  @inproceedings{BlGr00,
       author = {A. Blumensath and E. Grädel},
       title = {Automatic Structures},
       booktitle = {Proceedings of 15th IEEE Symposium on Logic in Computer Science LICS 2000},
       year = {2000},
       pages = {51–62},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/BlGr-lics00.ps},
  }
  

• J. Duparc. Anti-chains of mappings from $\omega^\omega$ on some BQO. 2000.                                 
  Abstract   BibTeX

  \bf Issue: Let $(P,\leq_P)$ be some BQO. Louveau and Saint-Raymond showed that the following structure $(\cal F, \leq_F)$ is also a BQO: $$\cal F=\\phi: \omega^{\omega\longmapsto P: \phi\mbox is Borel with countable image\}$$ with the usual topology on $\omega^\omega$ and the discrete topology on the BQO $P$; and $\phi\leq_F \psi$ iff there exists some continuous function $h: \omega^\omega\lmt\omega^\omega$ such that for all $x\in\omega^\omega$ $\phi(x)\leq_P\psi\circ h(x)$.

  The following proposition answers the question of the relation between cardinalities of anti-chains of $P$ and anti-chains of $\cal F$?

  @unpublished{JDns2,
       author = {J. Duparc},
       title = {Anti-chains of mappings from $\omega^\omega$ on some BQO},
       year = {2000},
       note = {Preprint, unpublished},
       url = {http://www.logic.rwth-aachen.de/pub/duparc/ns2.ps},
  }
  

• E. Gonçalvès and E. Grädel. Decidability issues for action guarded logics. In Proceedings of 2000 International Workshop on Description Logics – DL2000, pp. 123–132, 2000.             
  BibTeX

  @inproceedings{GoGr00,
       author = {E. Gonçalvès and E. Grädel},
       title = {Decidability issues for action guarded logics},
       booktitle = {Proceedings of 2000 International Workshop on Description Logics – DL2000},
       pages = {123–132},
       year = {2000},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/GoGr-dl00.ps},
  }
  

• G. Gottlob, E. Grädel, and H. Veith. Linear Time Datalog for Branching Time Logic. In Logic-Based Artificial Intelligence (J. Minker, Ed.). Kluwer, 2000.             
  BibTeX

  @incollection{GoGrVe00,
       author = {G. Gottlob and E. Grädel and H. Veith},
       title = {Linear Time Datalog for Branching Time Logic},
       booktitle = {Logic-Based Artificial Intelligence},
       editor = {J. Minker},
       chapter = {19},
       publisher = {Kluwer},
       year = {2000},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/GoGrVe-minker00.ps},
  }
  

• E. Grädel, C. Hirsch, and M. Otto. Back and Forth Between Guarded and Modal Logics. In Proceedings of 15th IEEE Symposium on Logic in Computer Science LICS 2000, pp. 217–228, Santa Barbara, 2000.                                 
  Abstract   BibTeX

  We propose a second-order extension for the guarded fragment showing that several canonical extensions are in fact equivalent. Then we ask the question in how far results from the modal world can be brought into the world of guarded logics. We give a transformation from first-order structures to Kripke type transition systems. This is used here to transform a theorem due to Janin and Walukiewicz about the expressive completeness of fixed-point logic in the context of bisimulation invariance.

  @inproceedings{GrHiOt00,
       author = {E. Grädel and C. Hirsch and M. Otto},
       title = {Back and Forth Between Guarded and Modal Logics},
       booktitle = {Proceedings of 15th IEEE Symposium on Logic in Computer Science LICS 2000},
       year = {2000},
       address = {Santa Barbara},
       pages = {217–228},
       note = {See also: journal version \citeGrHiOt00a},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/GrHiOt-lics00.ps},
  }
  

• C. Hirsch and S. Tobies. A Tableau Algorithm for the Clique Guarded Fragment. In Proceedings of the Workshop Advances in Modal Logic AiML 2000, Leipzig, Germany, 2000.             
  BibTeX

  @inproceedings{HT00,
       author = {C. Hirsch and S. Tobies},
       title = {A Tableau Algorithm for the Clique Guarded Fragment},
       booktitle = {Proceedings of the Workshop Advances in Modal Logic AiML 2000},
       year = {2000},
       address = {Leipzig, Germany},
       url = {http://www.logic.rwth-aachen.de/pub/hirsch/hito00.ps.gz},
  }
  

• S. Kreutzer. Fixed-point Query Languages for Linear Constraint Databases. In Proceedings of the 19th ACM Symp. on Principles of Database Systems (PODS), 2000, pp. 116–125. ACM press, 2000.                                 
  Abstract   BibTeX

  We introduce a family of query languages for linear constraint databases over the reals. The languages are defined over two-sorted structures, the first sort being the real numbers and the second sort consisting of a decomposition of the input relation into regions. The languages are defined as extensions of first-order logic by transitive closure or fixed-point operators, where the fixed-point operators are defined over the set of regions only. It is shown that the query languages capture precisely the queries definable in various standard complexity classes including PTIME.

  @inproceedings{Kreutzer00,
       author = {S. Kreutzer},
       title = {Fixed-point Query Languages for Linear Constraint Databases},
       booktitle = {Proceedings of the 19th ACM Symp. on Principles of Database Systems (PODS), 2000},
       pages = {116–125},
       year = {2000},
       publisher = {ACM press},
       url = {http://www.logic.rwth-aachen.de/pub/kreutzer/pods00.ps},
  }
  

• A. Nowack. Complexity Theory via Abstract State Machines. Diploma thesis, RWTH-Aachen, 2000.             
  BibTeX

  @misc{No00,
       author = {A. Nowack},
       title = {Complexity Theory via Abstract State Machines},
       howpublished = {Diploma thesis, RWTH-Aachen},
       year = {2000},
       url = {http://www.logic.rwth-aachen.de/pub/nowack/DiplArbeit.ps.gz},
  }
  

• E. Rosen and J. Tyszkiewicz. SO$(\forall\exists^*)$ sentences and their asymptotic probabilities. Mathematical Logic Quarterly, vol. 46, pp. 435–52, 2000.                                 
  Abstract   BibTeX

  We prove a 0-1 law for the fragment of second order logic SO(AE*) over parametric classes of structures which allow only one unary atomic type, confirming partially a conjecture of Lacoste. This completes the investigation of 0-1 laws for fragments of second order logic (with equality) defined in terms of first order quantifier prefixes over, e.g., simple graphs and tournaments. We also prove a low oscillation law, and establish the 0-1 law for $\Sigma_1^4(\forall\exists^*)$ without any restriction on the number of unary types.

  @article{RoTy00,
       author = {E. Rosen and J. Tyszkiewicz},
       title = {SO$(\forall\exists^*)$ sentences and their asymptotic probabilities},
       journal = {Mathematical Logic Quarterly},
       year = {2000},
       volume = {46},
       pages = {435–52},
       url = {http://www.logic.rwth-aachen.de/pub/rosen/ae.ps},
  }
  

• M. Spielmann. Model Checking Abstract State Machines and Beyond. In International Workshop on Abstract State Machines ASM 2000, LNCS, pp. 323–340. Springer-Verlag, 2000.                                 
  Abstract   BibTeX

  We propose a systematic investigation of the (semi-) automatic verifiability of ASMs. As a first step, we put forward two verification problems concerning the correctness of ASMs and investigate the decidability and complexity of both problems.

  @inproceedings{Sp00a,
       author = {M. Spielmann},
       title = {Model Checking Abstract State Machines and Beyond},
       booktitle = {International Workshop on Abstract State Machines ASM 2000},
       publisher = {Springer-Verlag},
       series = {LNCS},
       pages = {323–340},
       year = {2000},
       url = {http://www.logic.rwth-aachen.de/pub/spielmann/asm00.ps},
       copyright = {(c) Springer-Verlag},
  }
  

• M. Spielmann. Verification of Relational Transducers for Electronic Commerce. In 19th ACM Symposium on Principles of Database Systems PODS 2000, Dallas, pp. 92–93. ACM Press, 2000.                                 
  Abstract   BibTeX

  Motivated by recent work of Abiteboul, Vianu, Fordham, and Yesha [PODS`98] we investigate the verifiability of transaction protocols specifying the interaction of multiple parties via a network, where each party is equipped with an (active) database that participates in the interaction. Such transaction protocols typically occur in the context of electronic commerce applications and can be formalized as relational transducers. We introduce a class of powerful relational transducers based on Gurevich's abstract state machines and show that several verification problems related to electronic commerce applications can be solved for these transducers. Our approach is, in some sense, complementary to the approach in [PODS`98].

  @inproceedings{Sp00b,
       author = {M. Spielmann},
       title = {Verification of Relational Transducers for Electronic Commerce},
       booktitle = {19th ACM Symposium on Principles of Database Systems PODS 2000, Dallas},
       publisher = {ACM Press},
       year = {2000},
       pages = {92–93},
       url = {http://www.logic.rwth-aachen.de/pub/spielmann/pods00.ps},
  }
  

1999

• A. Blumensath. Automatic Structures. Diploma thesis, RWTH-Aachen, 1999.             
  BibTeX

  @misc{Bl99,
       author = {A. Blumensath},
       title = {Automatic Structures},
       howpublished = {Diploma thesis, RWTH-Aachen},
       year = {1999},
       url = {http://www.logic.rwth-aachen.de/pub/blume/AutStr.ps.gz},
  }
  

• J. Duparc. The normal form of Borel sets. Part II : Borel sets of infinite rank. Comptes Rendus de l'Académie des Sciences, pp. 735–740, 1999.                                 
  Abstract   BibTeX

  For each Borel set of reals of infinite rank $A$ we obtain a normal form of $A$ by finding a Borel set $\Omega$ such that $A$ and $\Omega$ continuously reduce to each other. We do so by defining simple Borel operations which are homomorphic to the $\omega_1$ first Veblen ordinal operations of base $\omega_1$ required to compute the Wadge degree of a Borel set.

  @article{JDcras2,
       author = {J. Duparc},
       title = {The normal form of Borel sets. Part II : Borel sets of infinite rank},
       journal = {Comptes Rendus de l'Académie des Sciences},
       year = {1999},
       number = {328},
       series = {I},
       pages = {735–740},
       url = {http://www.logic.rwth-aachen.de/pub/duparc/cras2.ps},
  }
  

• E. Grädel. Why are modal logics so robustly decidable? Bulletin of the European Association for Theoretical Computer Science, vol. 68, pp. 90–103, 1999.             
  BibTeX

  @article{Gr99,
       author = {E. Grädel},
       title = {Why are modal logics so robustly decidable?},
       journal = {Bulletin of the European Association for Theoretical Computer Science},
       volume = {68},
       year = {1999},
       pages = {90–103},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/Gr-eatcs99.ps},
  }
  

• E. Grädel. Decision procedures for guarded logics. In Automated Deduction – CADE16. Proceedings of 16th International Conference on Automated Deduction, Trento, 1999, vol. 1632 of LNCS. Springer-Verlag, 1999.             
  BibTeX

  @inproceedings{Gr99b,
       author = {E. Grädel},
       title = {Decision procedures for guarded logics},
       booktitle = {Automated Deduction – CADE16. Proceedings of 16th International Conference on Automated Deduction, Trento, 1999},
       publisher = {Springer-Verlag},
       series = {LNCS},
       volume = {1632},
       year = {1999},
       page = {31–51},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/Gr-cade99.ps},
       copyright = {(c) Springer-Verlag},
  }
  

• E. Grädel. On the restraining power of guards. Journal of Symbolic Logic, vol. 64, pp. 1719–1742, 1999.             
  BibTeX

  @article{Gr99d,
       author = {E. Grädel},
       title = {On the restraining power of guards},
       journal = {Journal of Symbolic Logic},
       volume = {64},
       year = {1999},
       pages = {1719–1742},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/Gr-jsl99.ps},
  }
  

• E. Grädel and S. Kreutzer. Descriptive Complexity Theory for Constraint Databases. In Proceedings of the Annual Conference of the European Association for Computer Science Logic, CSL `99, Madrid, vol. 1683 of LNCS, pp. 67–81. Springer-Verlag, 1999.                                 
  Abstract   BibTeX

  We consider the data complexity of various logics on two important classes of constraint databases: dense order and linear constraint databases. For dense order databases, we present a general result allowing us to lift results on logics capturing complexity classes from the class of finite ordered databases to dense order constraint databases. Considering linear constraints, we show that there is a significant gap between the data complexity of first-order queries on linear constraint databases over the real and the natural numbers. This is done by proving that for arbitrary high levels of the Presburger arithmetic there are complete first-order queries on databases over $(\mathbbN, <, +)$. The proof of the theorem demonstrates a simple argument for translating complexity results for prefix classes in logical theories to results on the complexity of query evaluation in constraint databases.

  @inproceedings{GrKr99,
       author = {E. Grädel and S. Kreutzer},
       title = {Descriptive Complexity Theory for Constraint Databases},
       booktitle = {Proceedings of the Annual Conference of the European Association for Computer Science Logic, CSL `99, Madrid},
       publisher = {Springer-Verlag},
       series = {LNCS},
       volume = {1683},
       year = {1999},
       pages = {67–81},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/GrKr-csl99.ps},
       copyright = {(c) Springer-Verlag},
  }
  

• E. Grädel and A. Malmström. 0-1 Laws for Recursive Structures. Archive for Mathematical Logic, vol. 38, pp. 205–215, 1999.                                 
  Abstract   BibTeX

  We discuss resource-bounded measures on the class of recursive structures and prove that with respect to such measures a random recursive structure is almost surely isomorphic to the unique countable model of the extension axioms.

  @article{GrMa99,
       author = {E. Grädel and A. Malmström},
       title = {0-1 Laws for Recursive Structures},
       journal = {Archive for Mathematical Logic},
       volume = {38},
       year = {1999},
       pages = {205–215},
       url = {http://www.logic.rwth-aachen.de/pub/anders/recursive.ps},
  }
  

• E. Grädel. The decidability of guarded fixed point logic. In JFAK. Essays Dedicated to Johan van Benthem on the Occasion of his 50th Birthday (J. Gerbrandy, M. Marx, M. de Rijke, and Y. Venema, Eds.). Amsterdam University Press, 1999.                                 
  Abstract   BibTeX

  Guarded fixed point logics are obtained by adding least and greatest fixed points to the guarded fragments of first-order logic that were recently introduced by Andreka, van Benthem and Nemeti. Guarded fixed point logics can also be viewed as the natural common extensions of the modal mu-calculus and the guarded fragments. In a joint paper with Igor Walukiewicz, we proved recently that the satisfiability problems for guarded fixed point logics are decidable and complete for deterministic double exponential time. That proof relies on alternating automata on trees and on a forgetful determinacy theorem for games on graphs with unbounded branching. We present here an elementary proof for the decidability of guarded fixed point logics which is based on guarded bisimulations, a tree model property for guarded logics and an interpretation into the monadic second-order theory of countable trees.

  @incollection{Gr99c,
       author = {E. Grädel},
       title = {The decidability of guarded fixed point logic},
       booktitle = {JFAK. Essays Dedicated to Johan van Benthem on the Occasion of his 50th Birthday},
       editor = {J. Gerbrandy and M. Marx and M. de Rijke and Y. Venema},
       publisher = {Amsterdam University Press},
       year = {1999},
       url = {http://turing.wins.uva.nl/~j50/cdrom/contribs/graedel/index.html},
  }
  

• E. Grädel and M. Otto. On Logics with Two Variables. Theoretical Computer Science, vol. 224, pp. 73–113, 1999.                                 
  Abstract   BibTeX

  Logical languages whose leading feature lies in the restriction to just two element variables play an important role in a number of applications, including the specification of processes or of the temporal or causal behaviour of transition systems, as well as the formalization of epistemological or terminological dependencies. The two-variable nature of many important languages may be attributed to the fact that they contain propositional modal logic as an essential core. Diverse mechanisms for extending basic modal logic have been analyzed with great success within the modal framework, and have lead to interesting, manageable languages, that meet the essential expressive needs for certain applications. For many applications, however, first-order closure properties offer an equally desirable direction for extensions. In this case, the extension of basic modal logic to first-order logic with two variables provides the natural starting point. This survey presents an overview of recent results pertaining to logics that lift some of the prominent mechanisms of extension from the modal framework to the framework of two-variable first-order logic. Most strikingly, two-variable first-order logic turns out to be not nearly as robust as modal logic with respect to satisfiability; several seemingly weak extensions of two-variable first-oder in important directions turn out to be highly undecidable. One notable exception is the extension by counting quantifiers, which does provide a decidable common extension of graded modal logic and two-variable first order. Some of the resulting other logics, while being undecidable, do provide natural levels of expressiveness for model checking applications, journal-title their complexity is generally no worse than for the underlying modal variants.

  @article{GraedelOtto98,
       author = {E. Grädel and M. Otto},
       title = {On Logics with Two Variables},
       journal = {Theoretical Computer Science},
       volume = {224},
       year = {1999},
       pages = {73–113},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/GrOt-tcs99.ps},
  }
  

• E. Grädel, M. Otto, and E. Rosen. Undecidability Results on Two-Variable Logics. Archive for Mathematical Logic, vol. 38, pp. 213–354, 1999.                                 
  Abstract   BibTeX

  It is a classical result of Mortimer's that L$^2$, first-order logic with two variables, is decidable for satisfiability. It is shown that going beyond L$^2$ by adding any one of the following leads to an undecidable logic:

  – very weak forms of recursion, viz. transitive closure operations, or (restricted) monadic fixed-point operations

  – weak access to cardinalities, through the Härtig (or equicardinality) quantifier, or

  – a choice construct known as Hilbert's epsilon operator.

  In fact all these extensions of L$^2$ prove to be undecidable both for satisfiability, and for satisfiability in finite models. Moreover most of them are hard for $\Sigma_1^1$, the first level of the analytical hierachy, and thus have a much higher degree of undecidability than first-order logic.

  @article{GraedelOttoRosen98,
       author = {E. Grädel and M. Otto and E. Rosen},
       title = {Undecidability Results on Two-Variable Logics},
       journal = {Archive for Mathematical Logic},
       volume = {38},
       year = {1999},
       pages = {213–354},
       note = {See also: conference version \citeGraedelOttoRosen97a},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/gor.ps},
  }
  

• E. Grädel and E. Rosen. Preservation theorems for two-variable logic. Mathematical Logic Quarterly, vol. 45, pp. 315–325, 1999.                                 
  Abstract   BibTeX

  We show that the existential preservation theorem fails for FO$^2$, two-variable first-order logic. It is known that for all k > 2, FO$^k$ does not have an existential preservation theorem, so this settles the last open case, answering a question of Andreka, van Benthem, and Nemeti. In contrast, we prove that the homomorphism preservation theorem holds for FO$^2$.

  @article{GrRo99,
       author = {E. Grädel and E. Rosen},
       title = {Preservation theorems for two-variable logic},
       journal = {Mathematical Logic Quarterly},
       volume = {45},
       year = {1999},
       pages = {315–325},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/preservation.ps},
  }
  

• E. Grädel and E. Rosen. Two-variable descriptions of regularity. In Proceedings of 14th IEEE Symposium on Logic in Computer Science LICS `99, Trento, pp. 14–23, 1999.             
  BibTeX

  @inproceedings{GrRo99b,
       author = {E. Grädel and E. Rosen},
       title = {Two-variable descriptions of regularity},
       booktitle = {Proceedings of 14th IEEE Symposium on Logic in Computer Science LICS `99, Trento},
       year = {1999},
       pages = {14–23},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/GrRo-lics99.ps},
  }
  

• E. Grädel and M. Spielmann. Logspace Reducibility via Abstract State Machines. In World Congress on Formal Methods (FM `99) (J. Wing, J. Woodcock, and J. Davies, Eds.), vol. 1709 of LNCS, pp. 1738–1757. Springer-Verlag, 1999.                                 
  Abstract   BibTeX

  Logspace computable functions play an important role in many areas of computer science, most notably in complexity theory, where logspace computable functions constitute the standard notion of reducibility. However, logspace reductions are defined by means of Turing machines which work on bit-strings, whereas many problems arising in computer science are naturally viewed as problems on structures (e.g., graphs). Unfortunately, there is a problem with encoding structures as bit-strings. Often we do not want to distinguish between isomorphic structures. More precisely, we want to identify an instance of a problem with an isomorphism class of structures rather than with a single structure. But there is no known efficiently computable string-encoding of isomorphism classes of structures. The situation calls for a computation model that works directly on structures and does not distinguish between isomorphic structures. \par Here we present a notion of logspace reducibility among structures which is based on abstract state machines (ASM)–a computation model on structures that has the desired isomorphism-invariance property. Our reductions are logspace computable (due to the syntactic restrictions we impose on ASM-programs) and are equally expressive as the logic (FO+DTC) enriched with the ability to handle small sets. On ordered structures they precisely capture Logspace. Our work continues that of Blass, Gurevich and Shelah on the choiceless fragment of Ptime. Indeed, our reductions can be seen as the choiceless fragment of Logspace.

  @inproceedings{GrSp99,
       author = {E. Grädel and M. Spielmann},
       title = {Logspace Reducibility via Abstract State Machines},
       booktitle = {World Congress on Formal Methods (FM `99)},
       editor = {J. Wing and J. Woodcock and J. Davies},
       publisher = {Springer-Verlag},
       series = {LNCS},
       volume = {1709},
       year = {1999},
       pages = {1738–1757},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/GrSp-fm99.ps},
       copyright = {(c) Springer-Verlag},
  }
  

• E. Grädel and I. Walukiewicz. Guarded Fixed Point Logic. In Proceedings of 14th IEEE Symposium on Logic in Computer Science LICS `99, Trento, pp. 45–54, 1999.             
  BibTeX

  @inproceedings{GrWa99,
       author = {E. Grädel and I. Walukiewicz},
       title = {Guarded Fixed Point Logic},
       booktitle = {Proceedings of 14th IEEE Symposium on Logic in Computer Science LICS `99, Trento},
       year = {1999},
       pages = {45–54},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/GrWa-lics99.ps},
  }
  

• E. Hoogland, M. Marx, and M. Otto. Beth Definability for the Guarded Fragment. In Proceedings of LPAR'99, LNAI. Springer-Verlag, 1999.                                 
  Abstract   BibTeX

  We analyze the question of existence of asymptotic cumulative probabilities for monadic second order definable properties of finite algebras. We focus our attention on the directly representable varieties and on the variety of groups. We prove in a very strong way that some recently proven first-order $0–1$ laws and limit laws for these varieties cannot be extended to monadic second order logic. Namely, if the function (n,A)->$pr_n[A]$ assigning probabilities to structures is recursive, then the 0-1 law holds according to the sequence pr_n=$pr_1$,$pr_2$,... of probabilities iff asymptotically there exists pr-almost surely precisely one algebra. Similarly, the convergence law holds iff asymptotically there are no large algebras according to pr.

  @inproceedings{HooglandMarxOtto99,
       author = {E. Hoogland and M. Marx and M. Otto},
       title = {Beth Definability for the Guarded Fragment},
       booktitle = {Proceedings of LPAR'99},
       publisher = {Springer-Verlag},
       series = {LNAI},
       year = {1999},
       url = {http://www.logic.rwth-aachen.de/pub/otto/beth.ps},
       copyright = {(c) Springer-Verlag},
  }
  

• S. Kreutzer. Descriptive Complexity Theory for Constraint Databases. Diploma thesis, RWTH-Aachen, 1999.             
  BibTeX

  @misc{Kre99,
       author = {S. Kreutzer},
       title = {Descriptive Complexity Theory for Constraint Databases},
       howpublished = {Diploma thesis, RWTH-Aachen},
       year = {1999},
       url = {http://www.logic.rwth-aachen.de/pub/kreutzer/diplom.ps},
  }
  

• F. Neven, M. Otto, J. Tyszkiewicz, and V. den Bussche. Adding FOR-Loops to First-Order Logic. In Proceedings of ICDT'99, vol. 1540 of LNCS, pp. 58–69. Springer-Verlag, 1999.             
  BibTeX

  @inproceedings{NeOtTyVa99,
       author = {F. Neven and M. Otto and J. Tyszkiewicz and Van den Bussche},
       title = {Adding FOR-Loops to First-Order Logic},
       booktitle = {Proceedings of ICDT'99},
       publisher = {Springer-Verlag},
       series = {LNCS},
       volume = {1540},
       year = {1999},
       pages = {58–69},
  }
  

• M. Otto. Bounded-Variable Logics: Two, Three, and More. Archive for Mathematical Logic, vol. 38, pp. 235–256, 1999.                                 
  Abstract   BibTeX

  This study concerns the bounded variable logics $L^k$ (with $k$ variable symbols), and $C^k$ (with $k$ variables in the presence of first-order counting quantifiers). These fragments of infinitary logic are well known to provide an adequate logical framework for some important issues in finite model theory. This paper deals with a translation that associates equivalence of structures in the $k$-variable fragments with bisimulation equivalence between derived structures. Apart from a uniform and intuitively appealing treatment of these equivalences, this approach relates some interesting issues for the case of an arbitrary number of variables to the case of just three variables. Invertibility of the invariants for $C^3$, in particular, would imply a positive answer to the tempting conjecture that fixed-point logic with counting captures Ptime in the world of bounded variable logic with counting.

  @article{Ot99,
       author = {M. Otto},
       title = {Bounded-Variable Logics: Two, Three, and More},
       journal = {Archive for Mathematical Logic},
       volume = {38},
       year = {1999},
       pages = {235–256},
       url = {ftp://ftp.informatik.rwth-aachen.de/pub/FMT/otto/twothree.ps},
  }
  

• M. Otto. Bisimulation-Invariant Ptime and Higher-Dimensional mu-Calculus. Theoretical Computer Science, vol. 224, pp. 237–265, 1999.                                 
  Abstract   BibTeX

  Let \em bisimilar Ptime be the class of those monadic queries over finite Kripke structures that are in Ptime and closed under bisimulation equivalence. This class \em bisimilar Ptime has a natural logical characterisation: it is captured, in the sense of descriptive complexity, by the straightforward extension of propositional $\mu$-calculus to arbitrary finite dimension. Here $\mu$-calculus in dimension $k$ is based on modal logic with $k$-tuples of worlds as the new $k$-worlds, $k$ different accessibility relations, one for each component, and a $\mu$-operator. It is also shown that even 2-dimensional $\mu$-calculus does not have the finite model property, is undecidable for finite satisfiability, and $\Sigma^1_1$-hard for satisfiability.

  @article{Otto98b,
       author = {M. Otto},
       title = {Bisimulation-Invariant Ptime and Higher-Dimensional mu-Calculus},
       journal = {Theoretical Computer Science},
       volume = {224},
       year = {1999},
       pages = {237–265},
       url = {http://www.logic.rwth-aachen.de/pub/otto/bisimP.ps},
  }
  

• M. Otto. Eliminating Recursion in the $\mu$-Calculus. In Proceedings of STACS'99, vol. 1563 of LNCS, pp. 531–540. Springer-Verlag, 1999.                                 
  Abstract   BibTeX

  The following decision problem is analysed: given a formula of the modal mu-calculus, decide whether there is some formula of basic modal logic equivalent to it. It is shown that this problem is decidable, and indeed Exptime complete. The decidability proof can be given through a purely model theoretic reduction to the monadic second-order theory of the binary tree, or through an analysis of suitably adapted tree automata. The latter analysis also yields a decision procedure in deterministic exponential time.

  @inproceedings{Otto98e,
       author = {M. Otto},
       title = {Eliminating Recursion in the $\mu$-Calculus},
       booktitle = {Proceedings of STACS'99},
       publisher = {Springer-Verlag},
       series = {LNCS},
       volume = {1563},
       year = {1999},
       pages = {531–540},
       url = {http://www.logic.rwth-aachen.de/pub/otto/mllmu.ps},
       copyright = {(c) Springer-Verlag},
  }
  

• E. Rosen. An existential fragment of second order logic. Archive for Mathematical Logic, vol. 38, pp. 217–234, 1999.                                 
  Abstract   BibTeX

  In this paper, we examine an existential fragment of second order logic, SO(E), which consists of all those second order sentences in which all first order quantifiers are existential. In particular, we are interested in analyzing the expressive power of this logic over the class of finite structures. First, we establish the decidability of its satisfaction problem, using a theorem due to Nesetril and Rodl. We then prove some facts about the expressive power of SO(E) over finite structures. In particular, we show how the Nesetril and Rodl theorem can be used to obtain non-definability results. We also consider the finite variable fragments of SO(E), and use the same machinery to prove that they form a strict hierarchy. Finally, it is shown that for every purely relational finite model \textbfA whose signature contains a relation symbol of arity > 3, the property of containing a submodel isomorphic to \textbfA is not expressible by any SO(E) sentence containing less than |\textbfA| (reusable) first order variables.

  @article{Ro99,
       author = {E. Rosen},
       title = {An existential fragment of second order logic},
       journal = {Archive for Mathematical Logic},
       volume = {38},
       year = {1999},
       pages = {217–234},
       url = {http://www.logic.rwth-aachen.de/pub/rosen/archiv.ps},
  }
  

• M. Spielmann. Automatic Verification of Abstract State Machines. In Proceedings of 11th International Conference on Computer-Aided Verification (CAV `99), vol. 1633 of LNCS, pp. 431–442. Springer-Verlag, 1999.                                 
  Abstract   BibTeX

  Abstract state machines (ASMs) provide the basis of a successful methodology for specification and verification of software and hardware systems. Nevertheless, computer aided verification of ASM-programs has not yet been well-developed. In this paper we try to shed some light on the limits of automatic verifiability of ASM-programs. We introduce a class of restricted ASM-programs, which are called nullary programs, and provide an algorithm that decides whether a given nullary program satisfies a given correctness property (expressible in a CTL$^*$-like temporal logic) on all inputs. Our decision algorithm runs in PSPACE and we show that this is optimal. We also show that straightforward generalizations of nullary programs cannot be verified algorithmically, as some basic verification problems become undecidable.

  @inproceedings{Sp99,
       author = {M. Spielmann},
       title = {Automatic Verification of Abstract State Machines},
       booktitle = {Proceedings of 11th International Conference on Computer-Aided Verification (CAV `99)},
       publisher = {Springer-Verlag},
       series = {LNCS},
       volume = {1633},
       year = {1999},
       pages = {431–442},
       url = {http://www.logic.rwth-aachen.de/pub/spielmann/cav99.ps},
       copyright = {(c) Springer-Verlag},
  }
  

1998

• E. Grädel. Guarded fragments of first-order logic: a perspective for new description logics? In Proceedings of 1998 International Workshop on Description Logics DL `98, Trento. CEUR Electronic Workshop Proceedings, 1998.             
  BibTeX

  @inproceedings{Gr98,
       author = {E. Grädel},
       title = {Guarded fragments of first-order logic: a perspective for new description logics?},
       booktitle = {Proceedings of 1998 International Workshop on Description Logics DL `98},
       address = {Trento},
       year = {1998},
       publisher = {CEUR Electronic Workshop Proceedings},
       note = {Extended abstract},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/Gr-dl98.ps},
  }
  

• E. Grädel and Y. Gurevich. Metafinite Model Theory. Information and Computation, vol. 140, pp. 26–81, 1998.             
  BibTeX

  @article{GrGu98,
       author = {E. Grädel and Y. Gurevich},
       title = {Metafinite Model Theory},
       journal = {Information and Computation},
       volume = {140},
       year = {1998},
       pages = {26–81},
       note = {See also: \citeGrGu95a},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/infcomp.ps},
  }
  

• E. Grädel, Y. Gurevich, and C. Hirsch. The complexity of query reliability. In 17th ACM Symposium on Principles of Database Systems PODS `98, Seattle. ACM Press, 1998.             
  BibTeX

  @inproceedings{GrGuHi98,
       author = {E. Grädel and Y. Gurevich and C. Hirsch},
       title = {The complexity of query reliability},
       booktitle = {17th ACM Symposium on Principles of Database Systems PODS `98, Seattle},
       publisher = {ACM Press},
       year = {1998},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/GrGuHi-pods98.ps},
  }
  

• C. Hirsch. The Reliability of Database Queries. Diploma thesis, RWTH-Aachen, 1998.             
  BibTeX

  @misc{Hi98,
       author = {C. Hirsch},
       title = {The Reliability of Database Queries},
       howpublished = {Diploma thesis, RWTH-Aachen},
       year = {1998},
  }
  

• P. Kolaitis and M. Otto. On the Boundedness Problem for Two-Variable First-Order Logic. In Proceedings of IEEE Symposium on Logic in Computer Science LICS `98, 1998.                                 
  Abstract   BibTeX

  A positive first-order formula is bounded if the sequence of its stages converges to the least fixed point of the formula within a fixed finite number of steps independent of the input structure. The boundedness problem for a fragment of first-order logic asks: given a positive formula in the fragment, is it bounded? \par We investigate the boundedness problem for two-variable first-order logic, an otherwise very well-behaved and, in particular, decidable fragment of first-order logic. Our main result asserts that the boundedness problem for two-variable first-order logic is undecidable, even when restricted to negation-free and equality-free formulae with a single monadic predicate variable that occurs within the scopes of universal quantifiers only. This contrasts sharply with earlier decidability results for monadic Datalog programs, which amount to the decidability of boundedness for negation-free and equality-free existential first-order formulae with a single monadic predicate variable. \par Our main result has certain applications to circumscription, the most well-developed formalism of nonmonotonic reasoning. Specifically, we show that it is an undecidable problem to tell whether the circumscription of a given two-variable first-order formula is equivalent to a first-order formula.

  @inproceedings{KolaitisOtto98,
       author = {P. Kolaitis and M. Otto},
       title = {On the Boundedness Problem for Two-Variable First-Order Logic},
       booktitle = {Proceedings of IEEE Symposium on Logic in Computer Science LICS `98},
       year = {1998},
       url = {http://www.logic.rwth-aachen.de/pub/jurek/kaufmann.ps},
  }
  

• M. Otto. Two-Variable First-Order Logic over Ordered Domains. 1998.                                 
  Abstract   BibTeX

  The satisfiability problem for the two-variable fragment FO$^2$ of first-order logic is investigated over finite and infinite linearly ordered, respectively wellordered domains, as well as over finite and infinite domains in which one or several designated binary predicates are interpreted as arbitrary wellfounded relations. It is shown that FO$^2$ over ordered, respectively wellordered, domains or in the presence of one wellfounded relation, is decidable for satisfiability as well as for finite satisfiability. Actually the complexity of these decision problems is essentially the same as for plain unconstrained FO$^2$, namely non-deterministic exponential time. In contrast FO$^2$ becomes undecidable for satisfiability and for finite satisfiability, if a sufficiently large number of predicates are required to be interpreted as (even partial) orderings, wellorderings, or as arbitrary wellfounded relations. This undecidability result also entails the undecidability of the natural common extension of FO$^2$ and computation tree logic.

  @unpublished{Otto98c,
       author = {M. Otto},
       title = {Two-Variable First-Order Logic over Ordered Domains},
       year = {1998},
       url = {http://www.logic.rwth-aachen.de/pub/otto/fotord.ps},
  }
  

• M. Otto. Epsilon-Logic is More Expressive Than First-Order Logic over Finite Structures. 1998.                                 
  Abstract   BibTeX

  It is shown that there are properties of finite structures that are expressible with the use of Hilbert's epsilon-operator in a manner that does not depend on the actual interpretation for epsilon-terms, but not expressible in plain first-order. This observation strengthens a corresponding result of Gurevich, concerning the invariant use of an auxiliary ordering in first-order logic over finite structures. The present result also implies that certain non-deterministic choice constructs, which have been considered in database theory, properly enhance the expressive power of first-order logic even as far as deterministic queries are concerned, thereby answering a question raised by Abiteboul and Vianu.

  @unpublished{Otto98d,
       author = {M. Otto},
       title = {Epsilon-Logic is More Expressive Than First-Order Logic over Finite Structures},
       year = {1998},
       url = {http://www.logic.rwth-aachen.de/pub/otto/epsilon.ps},
  }
  

• M. Otto. An interpolation theorem. 1998.                                 
  Abstract   BibTeX

  A relativized variant of Lyndons's Interpolation Theorem is proved, which gives a tool to focus on existential and universal quantification over designated subdomains – through positive and negative occurrences of predicates denoting these subdomains in relativized quantifications. It is shown how this single new interpolation theorem unifies a number of related results: namely, the classical preservation theorems concerning extensions/substructures with those concerning monotonicity, as well as a many-sorted interpolation theorem focusing on existentially/universally quantified sorts.

  @unpublished{Otto98f,
       author = {M. Otto},
       title = {An interpolation theorem},
       note = {Preprint, unpublished},
       year = {1998},
       url = {http://www.logic.rwth-aachen.de/pub/otto/int.ps},
  }
  

• E. Rosen. On the first-order prefix hierarchy. 1998.                                 
  Abstract   BibTeX

  We investigate the expressive power of fragments of first-order logic that are defined in terms of prefixes. The main result establishes a strict hierarchy among those fragments over the signature of a single binary relation. It implies that for each prefix $p$, there is a sentence $\phi_p$ in prefix normal form with prefix $p$, over a single binary relation, such that for all sentences $\theta$ in prenex normal form, of $\theta$ is equivalent to $\phi_p$, then $p$ can be embedded in the prefix of $\theta$. This strengthens a theorem of Walkoe.

  @misc{Rosen98,
       author = {Eric Rosen},
       title = {On the first-order prefix hierarchy},
       year = {1998},
       annote = {Preprint},
       url = {http://www.logic.rwth-aachen.de/pub/rosen/Rosen98.ps},
  }
  

• J. Tyszkiewicz. On the Kolmogorov Expressive Power of Boolean Query Languages. Theoretical Computer Science, vol. 190, pp. 317–361, 1998.                                 
  Abstract   BibTeX

  We address the question ''How much of the information stored in a given database can be retrieved by all Boolean queries in a given query language?'' In order to answer it we develop a Kolmogorov complexity based measure of expressive power of Boolean query languages over finite structures. This turns the above informal question into a precisely defined mathematical one. This notion gives a meaningful definition of the expressive power of a Boolean query language in a single finite database. \par The notion of Kolmogorov expressive power of a Boolean query language L in a finite database A is defined by considering two values: the Kolmogorov complexity of the isomorphism type of A, equal to the length of the shortest description of this type, and the number of bits of this description that can be reconstructed from truth values of all queries from L in A. The closer is the second value to the first, the more expressive is the query language. \par After giving the definitions and proving that they are correct, we concentrate our efforts on first order logic and its powerful extensions: inflationary fixpoint logic and partial fixpoint logic. We explore some connections between the proposed Kolmogorov expressive power of Boolean queries in these languages and their standard expressive power, in particular with the definability of order. We show that, except of being of interest for its own, our notion may have important diagnostic value for database query optimization.

  @article{Ty98,
       author = {J. Tyszkiewicz},
       title = {On the Kolmogorov Expressive Power of Boolean Query Languages},
       journal = {Theoretical Computer Science},
       volume = {190},
       year = {1998},
       pages = {317–361},
       note = {See also: Proceedings of International Conference in Database Theory ICDT `95, Lecture Notes in Computer Science No. 893, Springer-Verlag 1995, 97–110.},
       url = {http://www.logic.rwth-aachen.de/pub/jurek/kol.ps},
       copyright = {(c) Springer-Verlag},
  }
  

1997

• E. Börger, E. Grädel, and Y. Gurevich. The Classical Decision Problem. Springer-Verlag, 1997.             
  BibTeX

  @book{BoGrGu97,
       author = {E. Börger and E. Grädel and Y. Gurevich},
       title = {The Classical Decision Problem},
       publisher = {Springer-Verlag},
       year = {1997},
       series = {Perspectives of Mathematical Logic},
       url = {http://www.logic.rwth-aachen.de/Books/},
       note = {Second printing (Universitext) 2001.},
  }
  

• E. Grädel, P. Kolaitis, and M. Vardi. On the Decision Problem for Two-Variable First-Order Logic. Bulletin of Symbolic Logic, vol. 3, pp. 53–69, 1997.                                 
  Abstract   BibTeX

  We identify the computational complexity of the satisfiability problem for FO$^2$, the fragment of first-order logic consisting of all relational first-order sentences with at most two distinct variables. Although this fragment was shown to be decidable a long time ago, the computational complexity of its decision problem has not been pinpointed so far. In 1975 Mortimer proved that FO$^2$ is finitely controllable, which means that if an FO$^2$-sentence is satisfiable, then it has a finite model. Moreover, Mortimer showed that every satisfiable FO$^2$-sentence has a model whose size is at most doubly exponential in the size of the sentence. In this paper, we improve Mortimer's bound by one exponential and show that every satisfiable FO$^2$-sentence has a model whose size is at most exponential in the size of the sentence. As a consequence, we establish that the satisfiability problem for FO$^2$ is NEXPTIME-complete.

  @article{GrKoVa97,
       author = {E. Grädel and P. Kolaitis and M. Vardi},
       title = {On the Decision Problem for Two-Variable First-Order Logic},
       journal = {Bulletin of Symbolic Logic},
       volume = {3},
       year = {1997},
       pages = {53–69},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/basl.ps},
  }
  

• E. Grädel, M. Otto, and E. Rosen. Two-Variable Logic with Counting is Decidable. In Proceedings of 12th IEEE Symposium on Logic in Computer Science LICS `97, Warschau, 1997.                                 
  Abstract   BibTeX

  The satisfiability problem for C2 is shown to be decidable. \par C$^2$ is first-order logic with only two variables in the presence of arbitrary counting quantifiers of the form ''there exist at least m''. It considerably extends L$^2$, plain first-order with only two variables, which is known to be decidable by a result of Mortimer. Unlike L$^2$, C$^2$ does not have the finite model property. As C$^2$ extends L$^2$ by expressive means for counting, significant applications arise from the fact that C$^2$ embeds corresponding counting extensions of modal logics.

  @inproceedings{GraedelOttoRosen97,
       author = {E. Grädel and M. Otto and E. Rosen},
       title = {Two-Variable Logic with Counting is Decidable},
       booktitle = {Proceedings of 12th IEEE Symposium on Logic in Computer Science LICS `97, Warschau},
       year = {1997},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/gorc2.ps},
  }
  

• E. Grädel, M. Otto, and E. Rosen. Undecidability Results on Two-Variable Logics. In Proceedings of 14th Symposium on Theoretical Aspects of Computer Science STACS`97, vol. 1200 of Lecture Notes in Computer Science, pp. 249–260, 1997.             
  BibTeX

  @inproceedings{GraedelOttoRosen97a,
       author = {E. Grädel and M. Otto and E. Rosen},
       title = {Undecidability Results on Two-Variable Logics},
       booktitle = {Proceedings of 14th Symposium on Theoretical Aspects of Computer Science STACS`97},
       series = {Lecture Notes in Computer Science},
       volume = {1200},
       year = {1997},
       pages = {249–260},
       note = {See also: journal version \citeGraedelOttoRosen98},
  }
  

• Y. Gurevich and M. Spielmann. Recursive Abstract State Machines. JUCS, vol. 3(4), pp. 233–246, 1997.                                 
  Abstract   BibTeX

  According to the ASM thesis, any algorithm is essentially a Gurevich abstract state machine. The only objection to this thesis, at least in its sequential version, has been that ASMs do not capture recursion properly. To this end, we suggest recursive ASMs.

  @article{GuSp97,
       author = {Y. Gurevich and M. Spielmann},
       title = {Recursive Abstract State Machines},
       journal = {JUCS},
       volume = {3},
       number = {4},
       year = {1997},
       pages = {233–246},
       url = {http://www.logic.rwth-aachen.de/pub/spielmann/jucs97.ps},
  }
  

• P. Idziak and J. Tyszkiewicz. Monadic Second Order Probabilities in Algebra. Directly Representable Varieties and Groups. In Logic and Random Structures, AMS (R. B. Boppana and J. F. Lynch, Eds.), DIMACS Series in Discrete Mathematics and Theoretical Computer Science, AMS, pp. 79–108, 1997.             
  BibTeX

  @inproceedings{IdTy97,
       author = {P. Idziak and J. Tyszkiewicz},
       title = {Monadic Second Order Probabilities in Algebra. Directly Representable Varieties and Groups},
       booktitle = {Logic and Random Structures, AMS},
       editor = {R. B. Boppana and J. F. Lynch},
       series = {DIMACS Series in Discrete Mathematics and Theoretical Computer Science, AMS},
       year = {1997},
       pages = {79–108},
  }
  

• A. Malmström. Logic and Approximation. PhD thesis, RWTH Aachen, 1997.             
  BibTeX

  @phdthesis{Ma97b,
       author = {A. Malmström},
       title = {Logic and Approximation},
       school = {RWTH Aachen},
       year = {1997},
       url = {http://www.logic.rwth-aachen.de/pub/anders/intro.ps},
  }
  

• A. Malmström. Optimization problems with approximation schemes. In Annual Conference of the European Association for Computer Science Logic CSL'96, Selected Papers, Utrecht (NL) (D. van Dalen and M. Bezem, Eds.), vol. 1258 of LNCS, pp. 316–333. Springer-Verlag, 1997.                                 
  Abstract   BibTeX

  In this paper we extend recent work about the relationship between the syntactic description of NP optimization problems and their approximation properties. In contrast to \textbfMax SNP we consider problems that take arbitrary weighted structures as input instances and we use the framework of Metafinite Model Theory \citeGrGu98 to get a more general definability theory of optimization problems. We define a new class and show that every problem in this class has a fully polynomial-time approximation scheme (FPTAS), i.e. can be approximated to every desired accuracy e in time polynomial in the size of the input and $1/e$. An example for a problem in this class is \textbfKnapsack.

  @inproceedings{Ma97,
       author = {A. Malmström},
       title = {Optimization problems with approximation schemes},
       booktitle = {Annual Conference of the European Association for Computer Science Logic CSL'96, Selected Papers, Utrecht (NL)},
       editor = {D. van Dalen and M. Bezem},
       publisher = {Springer-Verlag},
       series = {LNCS},
       volume = {1258},
       year = {1997},
       pages = {316–333},
       url = {http://www.logic.rwth-aachen.de/pub/anders/csl96.ps},
  }
  

• M. Otto. Canonization for Two Variables and Puzzles on the Square. Annals of Pure and Applied Logic, vol. 85, pp. 243–282, 1997.                                 
  Abstract   BibTeX

  We consider infinitary logic with only two variable symbols, both with and without counting quantifiers, $L^2$ and $C^2$. The main result is that finite relational structures admit PTIME canonization with respect to $L^2$ and $C^2$: there are polynomial time computable functors mapping finite relational structures to unique representatives of their equivalence class with respect to indistinguishability in either of these logics. In fact Ptime inverses are constructed for the natural Ptime invariants that characterize structures up to $L^2$- or $C^2$-equivalence, respectively. This yields a recursive representations of the classes of all Ptime boolean queries that are closed with respect to $L^2$–or $C^2$–equivalence.

  @article{Ot97,
       author = {M. Otto},
       title = {Canonization for Two Variables and Puzzles on the Square},
       journal = {Annals of Pure and Applied Logic},
       volume = {85},
       year = {1997},
       pages = {243–282},
  }
  

• M. Otto. Capturing Bisimulation-Invariant Ptime. In Proceedings of 4th Symposium on Logical Foundations of Computer Science, LFCS `97, vol. 1234 of LNCS, pp. 294–305. Springer-Verlag, 1997.             
  BibTeX

  @inproceedings{Ot97c,
       author = {M. Otto},
       title = {Capturing Bisimulation-Invariant Ptime},
       booktitle = {Proceedings of 4th Symposium on Logical Foundations of Computer Science, LFCS `97},
       publisher = {Springer-Verlag},
       series = {LNCS},
       volume = {1234},
       year = {1997},
       pages = {294–305},
  }
  

• M. Otto. Bounded variable logics and counting — A study in finite models. Springer-Verlag, 1997.                                 
  Abstract   BibTeX

  This is a comprehensive treatment of a variety of results on infinitary logics with a bounded number of variables, both with and without counting quantifiers, as well as on related fixed-point logics. The emphasis is on central issues in finite model theory and in particular on descriptive complexity. Despite its character as a research monograph the exposition is largely self-contained. Much room is given to connections with the existing body of work in this area. From the contents:

  – An introduction to the relevant notions from logic, model theory, and to the programme of descriptive complexity.

  – A systematic treatment of the relevant games and game-theoretic structural invariants.

  – The analysis of fixed-point logics, both with and without counting.

  – Canonization and inversion problems as an approach to capturing fragments of PTIME.

  – Capturing results for the two-variable fragments of PTIME.

  @book{Otto95b,
       author = {M. Otto},
       title = {Bounded variable logics and counting — A study in finite models},
       booktitle = {Lecture Notes in Logic},
       volume = {9},
       publisher = {Springer-Verlag},
       year = {1997},
       copyright = {(c) Springer-Verlag},
  }
  

• M. Otto. The Logic of Explicitly Representation-Invariant Circuits. Selected Papers of CSL `96, vol. 1258, pp. 369–384, 1997.             
  BibTeX

  @article{Ot97b,
       author = {M. Otto},
       title = {The Logic of Explicitly Representation-Invariant Circuits},
       journal = {Selected Papers of CSL `96},
       editor = {D. van Dalen and M. Bezem},
       publisher = {Springer-Verlag},
       series = {LNCS},
       volume = {1258},
       year = {1997},
       pages = {369–384},
  }
  

• E. Rosen. Modal logic over finite structures. Journal of Logic, Language and Information, vol. 6, pp. 427–439, 1997.                                 
  Abstract   BibTeX

  We investigate properties of propositional modal logic over the class of finite structures. In particular, we show that certain known preservation theorems remain true over this class. We prove that a class of finite models is defined by a first-order sentence and closed under bisimulations if and only if it is definable by a modal formula. We also prove that a class of finite models defined by a modal formula is closed under extensions if and only if it is defined by a \verb $\Diamond$-modal formula.

  @article{Ro97,
       author = {E. Rosen},
       title = {Modal logic over finite structures},
       journal = {Journal of Logic, Language and Information},
       volume = {6},
       year = {1997},
       pages = {427–439},
       url = {http://www.logic.rwth-aachen.de/pub/rosen/jolli.ps},
  }
  

• J. Tyszkiewicz. The Kolmogorov Expression Complexity of Logics. Information and Computation, vol. 135, pp. 113–135, 1997.                                 
  Abstract   BibTeX

  The merit of the paper is to propose a completely new notion of complexity of logics in finite-model theory. It is the Kolmogorov variant of the Vardi's expression complexity. We define it by considering the value of the Kolmogorov complexity C(L[A]) of the infinite string L[A] of all truth values of sentences of L in A. The higher is this value, the more expressive is the logic L in A. \par If D is a class of finite models, then the value of C(L[A]) over all A in D is a measure of expressive power of L in D. Namely, unboundedness of C(L[A])-C(L'[A]) for A in D implies nonexistence of a recursive interpretation of L in L'. A version of this statement with complexities modulo oracle implies nonexistence of any interpretation of L in L'. Thus the values C(L[A]) modulo oracles constitute an invariant of expressive power of logics over finite models, depending on their real (absolute) expressive power, and not on the syntax. \par We investigate our notion for fragments of the infinitary logic L_\infty\omega^\omega: least fixpoint logic LFP and partial fixpoint logic PFP. We prove a precise characterization of 0-1 laws for these logics in terms of a certain boundedness condition placed on C(L[A]). We get an extension of the notion of a 0-1 law by imposing an upper bound on the value of C(L[A]) growing not too fast with cardinality of A, which still implies inexpressibility results similar to those implied by 0-1 laws.\par We also discuss the classes D in which C(PFPk[A]) is very high. It appears that then PFP or its simple extension can define all the PSPACE subsets of D.

  @article{Ty97,
       author = {J. Tyszkiewicz},
       title = {The Kolmogorov Expression Complexity of Logics},
       journal = {Information and Computation},
       volume = {135},
       year = {1997},
       pages = {113–135},
       url = {http://www.logic.rwth-aachen.de/pub/jurek/iandc.ps},
  }
  

• J. Tyszkiewicz. A Note on the Kolmogorov Data Complexity and Nonuniform Logical Definitions. Information Processing Letters, vol. 64, pp. 187–195, 1997.                                 
  Abstract   BibTeX

  We present a definition of the Kolmogorov data complexity and show how to use it to improve some already known results about hierarchies of Lindström quantifiers.

  @article{Ty97b,
       author = {J. Tyszkiewicz},
       title = {A Note on the Kolmogorov Data Complexity and Nonuniform Logical Definitions},
       journal = {Information Processing Letters},
       volume = {64},
       year = {1997},
       pages = {187–195},
       url = {http://www.logic.rwth-aachen.de/pub/jurek/kd.ps},
  }
  

• J. Tyszkiewicz. Queries and Algorithms Computable by Polynomial Time Existential Reflective Machines. Fundamenta Informaticae, vol. 32, pp. 91–105, 1997.                                 
  Abstract   BibTeX

  We consider two kinds of reflective relational machines: the usual ones, which use first order queries, and existential reflective machines, which use only first order existential queries. We compare these two computation models. We build on already existing results for standard relational machines, obtained by Abiteboul, Papadimitriou and Vianu, so we prove only results for existential machines. First we show that for both standard and existential reflective machines the set of polynomial time computable Boolean queries consists precisely of all PSPACE computable queries. \par The we go farther and compare which classes of algorithms both kinds of machines represent. \par It appears that, unless PSPACE=PTIME^NP, there are PSPACE queries which cannot be computed by polynomial time existential reflective machines which use only polynomial amount of relational memory, while it is always possible for standard reflective machines. We conclude that existential reflective machines, although equivalent in expressive power to unrestricted machines, provide substantially worse algorithms than the latter. \par On the positive side, we demonstrate that the above quality difference does not affect computing of PTIME queries, what can be done by existential reflective machines in PTIME, even if we take into account query evaluation costs, as well. \par Therefore within PTIME we use finer distinctions of the quality of algorithms. We demonstrate that any existential reflective machine computing the transitive closure query must use at least (1-o(1))log n variables, while for reflective relational machines using full first order queries already 3 variables suffice.

  @article{Ty97c,
       author = {J. Tyszkiewicz},
       title = {Queries and Algorithms Computable by Polynomial Time Existential Reflective Machines},
       journal = {Fundamenta Informaticae},
       volume = {32},
       year = {1997},
       pages = {91–105},
       url = {http://www.logic.rwth-aachen.de/pub/jurek/erm.ps},
  }
  

• J. Tyszkiewicz. Fine Hierarchies of Generic Computation. In Proceedings of International Conference in Database Theory ICDT `97 (F. Afrati and P. Kolaitis, Eds.), vol. 1186 of LNCS, pp. 125–139. Springer-Verlag, 1997.                                 
  Abstract   BibTeX

  Suppose that you are a user of a commercial relational database, accessible over the Internet, whose owner has decided to copy the price lists of the US telephone companies – first order queries are for free just like local calls, because they are local by the theorem of Gaifman. All recursive queries, being potentially non-local, are charged, for simplicity let us assume \$ 1.00 for a Boolean query. Non-Boolean queries are certainly not allowed, because the user would require all the data to be sent to him by issuing the first order identity query, and then manipulate with it himself, without any pay. These are the rules. Well, what is your strategy, to compute all you want to know about the database, paying as little as possible? And how much will the total price be? \par We answer this question, showing that the question whether you can get your answer without any costs at depends on whether or not the theories of databases in the provided query language are finitely axiomatizable. \par Thus, assuming there is a limit on the number of variables allowed in queries, if the database query language is the fixpoint logic, you can get everything for free. When it is Datalog however, even with inequality and negation of the edb's, you have to pay. We present a method, which for graphs of $n$ vertices costs about \$ $log log n$. Thus querying a graph with 1 Terabyte vertices costs \$ 7.00. We demonstrate that this price cannot be substantially reduced without causing a large computational overhead.

  @inproceedings{Ty97d,
       author = {J. Tyszkiewicz},
       title = {Fine Hierarchies of Generic Computation},
       booktitle = {Proceedings of International Conference in Database Theory ICDT `97},
       editor = {F. Afrati and Ph. Kolaitis},
       publisher = {Springer-Verlag},
       series = {LNCS},
       volume = {1186},
       year = {1997},
       pages = {125–139},
       url = {http://www.logic.rwth-aachen.de/pub/jurek/fams.ps},
       copyright = {(c) Springer-Verlag},
  }
  

1996

• K. Compton and E. Grädel. Logical Definability of Counting Functions. Journal of Computer and System Sciences, vol. 53, pp. 283–297, 1996.             
  BibTeX

  @article{CoGr96,
       author = {K. Compton and E. Grädel},
       title = {Logical Definability of Counting Functions},
       journal = {Journal of Computer and System Sciences},
       volume = {53},
       year = {1996},
       pages = {283–297},
       note = {See also: conference version \citeCoGr94},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/counting.ps},
  }
  

• E. Grädel and G. McColm. Hierarchies in Transitive Closure Logic, Stratified Datalog and Infinitary Logic. Annals of Pure and Applied Logic, vol. 77, pp. 166–199, 1996.             
  BibTeX

  @article{GrMc96,
       author = {E. Grädel and G. McColm},
       title = {Hierarchies in Transitive Closure Logic, Stratified Datalog and Infinitary Logic},
       journal = {Annals of Pure and Applied Logic},
       volume = {77},
       year = {1996},
       pages = {166–199},
       note = {See also: conference version \citeGrMc92a},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/GrMcC-apal96.ps},
  }
  

• E. Grädel and K. Meer. Descriptive Complexity Theory over the Real Numbers. Mathematics of Numerical Analysis: Real Number Algorithms, vol. 32, pp. 381–403, 1996.             
  BibTeX

  @article{GrMe96,
       author = {E. Grädel and K. Meer},
       title = {Descriptive Complexity Theory over the Real Numbers},
       journal = {Mathematics of Numerical Analysis: Real Number Algorithms},
       series = {AMS Lectures in Applied Mathematics},
       editor = {J. Renegar and M. Shub and S. Smale},
       volume = {32},
       year = {1996},
       pages = {381–403},
       note = {See also: conference version \citeGrMe95},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/GrMe-amsAM96.ps},
  }
  

• M. Otto. The Expressive Power of Fixed-Point Logic with Counting. Journal of Symbolic Logic, vol. 61, pp. 147–176, 1996.                                 
  Abstract   BibTeX

  This is an investigation in finite model theory concerning the expressive power of the logic FP+Counting, the extension of first-order logic which is obtained through adding both the fixed-point constructor and the ability to count. The analysis is carried out in parallel along two entirely different lines. One employs an isomorphism preserving (`generic') model of computation, whose PTIME restriction exactly corresponds to FP+Counting, while its PSPACE restriction corresponds to WHILE+Counting. A normal form gives a clear separation of the relational vs. the arithmetical side of the algorithms involved. The other one uses the connection with the infinitary logics Cr, r-variable infinitary logic with counting quantifiers, to apply the corresponding pebble games in the analysis. \par The main result involves the concept of an arithmetical invariant. This is a functor taking every finite relational structure to an expansion of (an initial segment of) the standard arithmetical structure. A family of arithmetical invariants Ir with the following properties is introduced:

  – each $I^r$ can be evaluated in polynomial time.

  – a class of finite relational structures is definable in FP+Counting if and only if membership can be decided in polynomial time on the basis of the values of one of the invariants.

  – $I^r$ classifies all finite relational structures exactly up to equivalence with respect to the logic $C^r$.

  Further issues concern a characterization of FP+Counting in terms of those sequences of finitary formulae in the $C^r$ that are polynomial time computable, and a positive assessment of the expressive power of FP+Counting in comparison with related extensions of fixed-point logic by Lindström quantifiers. The extesnsion by all Lindström quantifiers, which capture PTIME computable properties of cardinalities of definable predicates, remains strictly weaker than FP+Counting. In particular, every extension of fixed-point logic by monadic Lindström quantifiers, which stays within PTIME, is strictly contained in FP+Counting.

  @article{Ot96,
       author = {M. Otto},
       title = {The Expressive Power of Fixed-Point Logic with Counting},
       journal = {Journal of Symbolic Logic},
       volume = {61},
       year = {1996},
       pages = {147–176},
  }
  

• M. Otto and J. V. den Bussche. First-Order Queries on Databases Embedded in an Infinite Structure. Information Processing Letters, vol. 60, pp. 37–41, 1996.             
  BibTeX

  @article{OtVa96,
       author = {M. Otto and J. Van den Bussche},
       title = {First-Order Queries on Databases Embedded in an Infinite Structure},
       journal = {Information Processing Letters},
       volume = {60},
       year = {1996},
       pages = {37–41},
  }
  

1995

• A. Dawar and E. Grädel. Generalized Quantifiers and 0-1 Laws. In Proceedings of 10th IEEE Symposium on Logic in Computer Science LICS `95, San Diego, pp. 54–64, 1995.             
  BibTeX

  @inproceedings{DaGr95,
       author = {A. Dawar and E. Grädel},
       title = {Generalized Quantifiers and 0-1 Laws},
       booktitle = {Proceedings of 10th IEEE Symposium on Logic in Computer Science LICS `95, San Diego},
       year = {1995},
       pages = {54–64},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/lics95.ps},
  }
  

• J. Duparc. The normal form of Borel sets. Part I: Borel sets of finite rank. Comptes Rendus de l'Académie des Sciences, pp. 651–656, 1995.                                 
  Abstract   BibTeX

  For each Borel set of reals A, of finite rank, we obtain a ''normal form'' of A, by finding a Borel set $\Omega$ of maximum simplicity, such that A and $\Omega$ continuously reduce to each other. In more technical terms : we define simple Borel operations which are homomorphic to ordinal sum, to multiplication by a countable ordinal, and to ordinal exponentiation of base $\omega_1$, under the map which sends every Borel set A of finite rank to its Wadge degree.

  @article{JDcras1,
       author = {J. Duparc},
       title = {The normal form of Borel sets. Part I: Borel sets of finite rank},
       journal = {Comptes Rendus de l'Académie des Sciences},
       year = {1995},
       number = {320},
       series = {I},
       pages = {651–656},
       url = {http://www.logic.rwth-aachen.de/pub/duparc/cras1.ps},
  }
  

• J. Duparc. La forme normale des Boréliens de rangs finis. PhD thesis, Université Paris VII, 1995.             
  BibTeX

  @phdthesis{JDphd,
       author = {J. Duparc},
       title = {La forme normale des Boréliens de rangs finis},
       year = {1995},
       month = {July},
       school = {Université Paris VII},
       note = {In French},
  }
  

• E. Grädel and Y. Gurevich. Tailoring Recursion for Complexity. Journal of Symbolic Logic, vol. 60, pp. 952–969, 1995.             
  BibTeX

  @article{GrGu95,
       author = {E. Grädel and Y. Gurevich},
       title = {Tailoring Recursion for Complexity},
       journal = {Journal of Symbolic Logic},
       volume = {60},
       year = {1995},
       pages = {952–969},
       note = {See also: conference version \citeGrGu94},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/tailoring.ps},
  }
  

• E. Grädel and Y. Gurevich. Metafinite Model Theory. In Logic and Computational Complexity, Selected Papers (D. Leivant, Ed.), pp. 213–366. Springer-Verlag, 1995.             
  BibTeX

  @inproceedings{GrGu95a,
       author = {E. Grädel and Y. Gurevich},
       title = {Metafinite Model Theory},
       booktitle = {Logic and Computational Complexity, Selected Papers},
       editor = {D. Leivant},
       publisher = {Springer-Verlag},
       year = {1995},
       pages = {213–366},
       note = {See also: journal version \citeGrGu98},
  }
  

• E. Grädel and G. McColm. On the Power of Deterministic Transitive Closures. Information and Computation, vol. 119, pp. 129–135, 1995.             
  BibTeX

  @article{GrMc95,
       author = {E. Grädel and G. McColm},
       title = {On the Power of Deterministic Transitive Closures},
       journal = {Information and Computation},
       volume = {119},
       year = {1995},
       pages = {129–135},
       note = {See also: conference version \citeGrMc92},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/GrMcC-ic95.ps},
  }
  

• E. Grädel and K. Meer. Descriptive Complexity Theory over the Real Numbers. In Proceedings of the 27th ACM-Symposium on Theory of Computing, STOC 95, Las Vegas, 1995.             
  BibTeX

  @inproceedings{GrMe95,
       author = {E. Grädel and K. Meer},
       title = {Descriptive Complexity Theory over the Real Numbers},
       booktitle = {Proceedings of the 27th ACM-Symposium on Theory of Computing, STOC 95},
       address = {Las Vegas},
       year = {1995},
       note = {See also: journal version \citeGrMe96},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/stoc95.ps},
  }
  

• A. Malmström. Log-approximable minimization problems on random input. In Annual Conference of the European Association for Computer Science Logic CSL'94, Selected Papers, Kazimierz (Poland), vol. 933 of LNCS, pp. 217–227. Springer-Verlag, 1995.                                 
  Abstract   BibTeX

  We extend recent work about the relationship between logically defined classes of NP optimization problems and the asymptotic growth of optimal solutions on random inputs. We consider the syntactic class $MinF+\Pi_2(1)$ of minimization problems. Kolaitis and Thakur proved that every problem in this class is log-approximable. We show that for every problem Q in the class Min $F+\Pi_2(1)$ there exist polynomials $g(n)$ and $h(n)$ such the optimal solution of Q almost surely grows like $\Theta (g(n)+h(n) log n)$. Applying this result we show without using any complexity theoretical assumptions that the problem \textbfMin Graph Colouring is not in $Min F+\Pi_2(1)$. With the same method we get a similar criterion for each class $Min F+Pi_2(k)$. Using the fact that on a random graph with n nodes the chromatic number is $n/(2log n)$ almost surely we prove that \textbfMin Graph Colouring is not in $Min F+\Pi_2$, resolving a conjecture by Kolaitis and Thakur.

  @inproceedings{Ma95,
       author = {A. Malmström},
       title = {Log-approximable minimization problems on random input},
       booktitle = {Annual Conference of the European Association for Computer Science Logic CSL'94, Selected Papers, Kazimierz (Poland)},
       publisher = {Springer-Verlag},
       series = {LNCS},
       volume = {933},
       year = {1995},
       pages = {217–227},
       url = {http://www.logic.rwth-aachen.de/pub/anders/csl94.ps},
  }
  

• M. Otto. Bounded variable logics and counting — A study in finite models. 1995.             
  BibTeX

  @misc{Ot95,
       author = {M. Otto},
       title = {Bounded variable logics and counting — A study in finite models},
       note = {Habilitationsschrift RWTH Aachen, 190 pages. See also: monograph \citeOtto95b},
       year = {1995},
  }
  

• M. Otto. A note on the number of monadic quantifiers in monadic $\Sigma^1_1$. Information Processing Letters, vol. 53(6), pp. 337–339, 1995.                                 
  Abstract   BibTeX

  A simple proof is given, that the number of monadic quantifiers in existential monadic second-order logic gives rise to a strict hierarchy over finite structures. This resolves a problem put forward by R.Fagin.

  @article{Ot95c,
       author = {Martin Otto},
       title = {A note on the number of monadic quantifiers in monadic $\Sigma^1_1$},
       journal = {Information Processing Letters},
       volume = {53},
       number = {6},
       pages = {337–339},
       day = {24},
       month = {March},
       year = {1995},
  }
  

• M. Otto. Ptime canonization for two variables with counting. In Proceedings of 10th IEEE Symposium on Logic in Computer Science LICS `95, pp. 342–352, 1995.                                 
  Abstract   BibTeX

  Infinitary logic with two variable symbols and counting quantifiers $C^2$ and its intersection with PTIME are considered on finite relational structures. A PTIME canonization procedure is presented which provides unique representatives up to equivalence in $C^2$ for finite relational structures. As a consequence there is a recursive presentation for the class of all those queries on arbitrary finite relational structures which are both PTIME and definable in $C^2$. The proof renders a succinct normal form representation of this non-trivial semantically defined fragment of PTIME. Through specializations of the proof techniques similar results apply with respect to the logic L2, infinitary logic with two variable symbols, itself.

  @inproceedings{Ot95d,
       author = {M. Otto},
       title = {Ptime canonization for two variables with counting},
       booktitle = {Proceedings of 10th IEEE Symposium on Logic in Computer Science LICS `95},
       year = {1995},
       pages = {342–352},
       url = {http://www.logic.rwth-aachen.de/pub/otto/LICS95.ps},
  }
  

• J. Tyszkiewicz. Probabilities in First-Order Logic of a Unary Function and a Binary Relation. Random Structures and Algorithms, vol. 6, pp. 181–191, 1995.                                 
  Abstract   BibTeX

  We settle the question of the behaviour of probabilities of sentences of first-order logic about a unary function and a binary relation. We show that there are sentences of this logic without asymptotic probability. \par This settles the last open case in the problem of establishing the behaviour of asymptotic probabilities for classes of labelled structures corresponding to natural signatures.

  @article{Ty95,
       author = {J. Tyszkiewicz},
       title = {Probabilities in First-Order Logic of a Unary Function and a Binary Relation},
       journal = {Random Structures and Algorithms},
       volume = {6},
       year = {1995},
       pages = {181–191},
  }
  

1994

• K. Compton and E. Grädel. Logical Definability of Counting Functions. In Proceedings of 9th IEEE Conference on Structure in Complexity Theory, pp. 255–266, Amsterdam, 1994.             
  BibTeX

  @inproceedings{CoGr94,
       author = {K. Compton and E. Grädel},
       title = {Logical Definability of Counting Functions},
       booktitle = {Proceedings of 9th IEEE Conference on Structure in Complexity Theory},
       pages = {255–266},
       year = {1994},
       address = {Amsterdam},
       note = {See also: journal version \citeCoGr96},
  }
  

• J. Duparc. A normal form for Borel sets. 1994.                                 
  Abstract   BibTeX

  For each Borel set $A$ of reals, or more generally of infinite strings from a countable alphabet, we obtain a normal form of $A$, by finding a Borel set $\Omega$ of maximum simplicity, such that $A$ and $\Omega$ continuously reduce to each other. $\Omega$ only depend on the equivalence class of $A$ modulo inter-reducibility, moreover, the map: $A\longmapsto\Omega$ is defined in a simple way (in $ZF+DC$). In case of Borel sets of finite rank, we prove the above result essentially by defining simple Borel operations which are homomorphic to ordinal sum, to multiplication by a countable ordinal, and to ordinal exponentiation of base $\omega_1$ (under the map which sends every Borel set $A$ of finite rank to its Wadge degree). Extension to transfinite ranks is provided by iterating both ordinal exponentiation and its Borel counterpart. And finally, we show that all these results can be extended to all Borel subsets of $X^\omega$ when the alphabet $X$ is of any cardinal.

  @unpublished{JDns3,
       author = {J. Duparc},
       title = {A normal form for Borel sets},
       year = {1994},
       note = {Extended abstract},
       url = {http://www.logic.rwth-aachen.de/pub/duparc/ns3.ps},
  }
  

• E. Grädel. Definability on Finite Structures and the Existence of One-Way Functions. Methods of Logic in Computer Science, vol. 1, pp. 299–314, 1994.             
  BibTeX

  @article{Gr94,
       author = {E. Grädel},
       title = {Definability on Finite Structures and the Existence of One-Way Functions},
       journal = {Methods of Logic in Computer Science},
       volume = {1},
       year = {1994},
       pages = {299–314},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/Gr-mlcs94.ps},
  }
  

• E. Grädel and Y. Gurevich. Tailoring Recursion for Complexity. In Proceedings of 21st International Colloquium on Automata, Languages and Programming ICALP 94, vol. 820 of LNCS, pp. 118–129. Springer-Verlag, 1994.             
  BibTeX

  @inproceedings{GrGu94,
       author = {E. Grädel and Y. Gurevich},
       title = {Tailoring Recursion for Complexity},
       booktitle = {Proceedings of 21st International Colloquium on Automata, Languages and Programming ICALP 94},
       series = {LNCS},
       volume = {820},
       publisher = {Springer-Verlag},
       year = {1994},
       pages = {118–129},
       note = {See also: journal version \citeGrGu95},
  }
  

• E. Grädel and A. Malmström. Approximable minimization problems and optimal solutions on random input. In Computer Science Logic, 7th Workshop, CSL `93, Swansea 1993, Selected Papers (E. Börger, Y. Gurevich, and K. Meinke, Eds.), vol. 832 of LNCS, pp. 139–149. Springer-Verlag, 1994.                                 
  Abstract   BibTeX

  In this paper we extend recent work about logical criteria for approximation properties of optimization problems. We focus on the relationship between logical expressibility and expected asymptotic growth of optimal solutions on random inputs. This further develops a probabilistic approach due to Behrendt, Compton and Grädel showing that expected optimal solutions for any problem in the class Max Sigma1 grows essentially like a polynomial. We show that there is a similar result for Min $F+\Pi_1$, a syntactic class of minimization problems which provides a logical criterion for approximability. As a consequence, we show that some important problems do not belong to Min $F+\Pi_1$.

  @inproceedings{GrMa94,
       author = {E. Grädel and A. Malmström},
       title = {Approximable minimization problems and optimal solutions on random input},
       booktitle = {Computer Science Logic, 7th Workshop, CSL `93, Swansea 1993, Selected Papers},
       editor = {E. Börger and Y. Gurevich and K. Meinke},
       publisher = {Springer-Verlag},
       series = {LNCS},
       volume = {832},
       year = {1994},
       pages = {139–149},
       url = {http://www.logic.rwth-aachen.de/pub/anders/csl93.ps},
  }
  

• M. Otto. Generalized quantifiers for simple properties. In Proceedings of 9th IEEE Symposium on Logic in Computer Science LICS `94, pp. 30–39, 1994.                                 
  Abstract   BibTeX

  Extensions of fixed-point logic by means of generalized quantifiers are considered in the context of descriptive complexity. By the well-known theorem of Immerman and Vardi, fixed-point logic captures PTIME over linearly ordered structures. It fails, however, to express even most fundamental structural properties, like simple cardinality properties, in the absence of order. The present investigation concentrates on extensions by generalized quantifiers which serve to adjoin \em simple or \em basic structural properties. An abstract notion of simplicity is put forward which isolates those structural properties, that can be characterized in terms of a concise \em structural invariant. The key examples are provided by all monadic and cardinality properties in a very general sense. The main theorem establishes that no extension by any family of such simple quantifiers can cover all of PTIME. These limitations are proved on the basis of the semantically motivated notion of simplicity; in particular there is no implicit bound on the arities of the generalized quantifiers involved. Quite to the contrary, the natural applications concern infinite families of quantifiers adjoining certain structural properties across all arities in a uniform way.

  @inproceedings{Ot94,
       author = {M. Otto},
       title = {Generalized quantifiers for simple properties},
       booktitle = {Proceedings of 9th IEEE Symposium on Logic in Computer Science LICS `94},
       year = {1994},
       pages = {30–39},
       url = {http://www.logic.rwth-aachen.de/pub/otto/LICS94.ps},
  }
  

• M. Otto. Symmetry and First-Order: Explicitly Representation-Invariant Circuits. 1994.                                 
  Abstract   BibTeX

  Circuit complexity is considered under the additional assumption of full combinatorial symmetry with respect to permutations of the input representation. This approach leads to a very natural and simple characterization of first-order logic and its infinitary variant with bounded numbers of variables over finite structures. Extensions to not necessarily acyclic boolean networks provide corresponding characterizations of partial fixed-point logic (or the relational query language WHILE) and ordinary fixed-point logic.

  @unpublished{Ot94b,
       author = {M. Otto},
       title = {Symmetry and First-Order: Explicitly Representation-Invariant Circuits},
       note = {See also: journal version \citeOt97b},
       year = {1994},
       url = {http://www.logic.rwth-aachen.de/pub/otto/Circ.ps},
  }
  

• J. Tyszkiewicz. Infinitary queries and their asymptotic probabilities II: properties definable in least fixed point logic. Random Structures and Algorithms, vol. 5, pp. 215–234, 1994.                                 
  Abstract   BibTeX

  We develop an almost complete theory for existence of asymptotic probabilities of least fixed point and partial fixed point definable properties, and for the complexity of the associated almost sure theory. Our method works for any randomized class of finite structures.

  @article{Ty94,
       author = {J. Tyszkiewicz},
       title = {Infinitary queries and their asymptotic probabilities II: properties definable in least fixed point logic},
       journal = {Random Structures and Algorithms},
       volume = {5},
       year = {1994},
       pages = {215–234},
       url = {http://www.logic.rwth-aachen.de/pub/jurek/lfp.ps},
  }
  

1993

• T. Behrendt, K. Compton, and E. Grädel. Optimization Problems: Expressibility, Approximation Properties, and Expected Asymptotic Growth of Optimal Solutions. In Computer Science Logic, 6th Workshop, CSL `92, San Miniato 1992, Selected Papers (E. Börger, G. Jäger, H. K. Büning, S. Martini, and M. M. Richter, Eds.), vol. 702 of LNCS, pp. 43–60. Springer-Verlag, 1993.             
  BibTeX

  @inproceedings{BeCoGr93,
       author = {Th. Behrendt and K. Compton and E. Grädel},
       title = {Optimization Problems: Expressibility, Approximation Properties, and Expected Asymptotic Growth of Optimal Solutions},
       booktitle = {Computer Science Logic, 6th Workshop, CSL `92, San Miniato 1992, Selected Papers},
       editor = {E. Börger and G. Jäger and H. Kleine Büning and S. Martini and M. M. Richter},
       publisher = {Springer-Verlag},
       series = {LNCS},
       volume = {702},
       year = {1993},
       pages = {43–60},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/CSL-BCG.ps},
       copyright = {(c) Springer-Verlag},
  }
  

• E. Grädel and M. Otto. Inductive Definability with Counting on Finite Structures. In Computer Science Logic, 6th Workshop, CSL `92, San Miniato 1992, Selected Papers (E. Börger, G. Jäger, H. K. Büning, S. Martini, and M. M. Richter, Eds.), vol. 702 of LNCS, pp. 231–247. Springer-Verlag, 1993.                                 
  Abstract   BibTeX

  The properties and the expressive power of logical languages that include both a mechanism for inductive definitions and the ability to count are studied. The most important of these languages is fixed-point logic with counting terms, denoted FP+C. It is shown that in the presence of counting terms inductive definability on arbitrary finite structures has nice properties that it retains without counting only in the case of ordered structures. Main issues of the investigation concern:

  – equivalent charcterizations and robustness of FP+C: e.g. FP+C is equivalent with DATALOG+C and offers intuitive functional as well as machine theoretic characterizations.

  – relations with infinitary logic with bounded number of variables and counting quantifiers.

  – relations with partial fixed-point logic with counting, PFP+C.

  @inproceedings{GrOt93,
       author = {E. Grädel and M. Otto},
       title = {Inductive Definability with Counting on Finite Structures},
       booktitle = {Computer Science Logic, 6th Workshop, CSL `92, San Miniato 1992, Selected Papers},
       editor = {E. Börger and G. Jäger and H. Kleine Büning and S. Martini and M. M. Richter},
       publisher = {Springer-Verlag},
       series = {LNCS},
       volume = {702},
       year = {1993},
       pages = {231–247},
       url = {http://www.logic.rwth-aachen.de/pub/otto/CSL92.ps},
       copyright = {(c) Springer-Verlag},
  }
  

• J. Tyszkiewicz. On Asymptotic Probabilities in Logics That Capture DSPACE($\log n$) in Presence of Ordering. In Proceedings of TAPSOFT `93, vol. 668 of LNCS, pp. 569–583. Springer-Verlag, 1993.                                 
  Abstract   BibTeX

  We show that for logics that capture DSPACE(log n) over ordered structures, and for recursive probability distributions on the class of finite models of the signature, the 0-1 law and the convergence law hold if and only if certain boundedness conditions are satisfied. As one of the applications, we solve the conjecture of Kolaitis and Vardi stating that for arbitrary probability distributions the 0-1 law holds for the logic L^\omega_\infty\omega iff the same law holds for fixpoint logic.

  @inproceedings{Ty93b,
       author = {J. Tyszkiewicz},
       title = {On Asymptotic Probabilities in Logics That Capture DSPACE($\log n$) in Presence of Ordering},
       booktitle = {Proceedings of TAPSOFT `93},
       publisher = {Springer-Verlag},
       series = {LNCS},
       volume = {668},
       year = {1993},
       pages = {569–583},
       url = {http://www.logic.rwth-aachen.de/pub/jurek/caap.ps},
  }
  

• J. Tyszkiewicz. On Asymptotic Probabilities of Monadic Second Order Properties. In Computer Science Logic, 6th Workshop, CSL `92, San Miniato 1992, Selected Papers (E. Börger, G. Jäger, H. K. Büning, S. Martini, and M. M. Richter, Eds.), vol. 702 of LNCS, pp. 425–439. Springer-Verlag, 1993.                                 
  Abstract   BibTeX

  We propose a new, general and easy method for proving nonexistence of asymptotic probabilities of monadic second-order sentences in classes of finite structures where first-order extension axioms hold almost surely.

  @inproceedings{Ty93,
       author = {J. Tyszkiewicz},
       title = {On Asymptotic Probabilities of Monadic Second Order Properties},
       booktitle = {Computer Science Logic, 6th Workshop, CSL `92, San Miniato 1992, Selected Papers},
       editor = {E. Börger and G. Jäger and H. Kleine Büning and S. Martini and M. M. Richter},
       publisher = {Springer-Verlag},
       series = {LNCS},
       volume = {702},
       year = {1993},
       pages = {425–439},
       url = {http://www.logic.rwth-aachen.de/pub/jurek/csl-mail.ps},
       copyright = {(c) Springer-Verlag},
  }
  

1992

• E. Grädel. Capturing Complexity Classes by Fragments of Second Order Logic. Theoretical Computer Science, vol. 101, pp. 35–57, 1992.             
  BibTeX

  @article{Gr92,
       author = {E. Grädel},
       title = {Capturing Complexity Classes by Fragments of Second Order Logic},
       journal = {Theoretical Computer Science},
       volume = {101},
       year = {1992},
       pages = {35–57},
  }
  

• E. Grädel. On Transitive Closure Logic. In Proceedings of 5th Workshop on Computer Science Logic CSL `91, Bern 1991, vol. 626 of LNCS, pp. 149–163. Springer-Verlag, 1992.             
  BibTeX

  @inproceedings{Gr92b,
       author = {E. Grädel},
       title = {On Transitive Closure Logic},
       booktitle = {Proceedings of 5th Workshop on Computer Science Logic CSL `91, Bern 1991},
       publisher = {Springer-Verlag},
       series = {LNCS},
       volume = {626},
       year = {1992},
       pages = {149–163},
  }
  

• E. Grädel and G. McColm. Deterministic versus Nondeterministic Transitive Closure Logic. In Proceedings of 7th IEEE Symposium on Logic in Computer Science LICS `92, pp. 58–63, Santa Cruz, 1992.             
  BibTeX

  @inproceedings{GrMc92,
       author = {E. Grädel and G. McColm},
       title = {Deterministic versus Nondeterministic Transitive Closure Logic},
       booktitle = {Proceedings of 7th IEEE Symposium on Logic in Computer Science LICS `92},
       address = {Santa Cruz},
       year = {1992},
       pages = {58–63},
       note = {See also: journal version \citeGrMc95},
  }
  

• E. Grädel and G. McColm. Hierarchies in Transitive Closure Logic, Stratified Datalog and Infinitary Logic. In Proceedings of 33rd Annual IEEE Symposium on Foundations of Computer Science FOCS `92, pp. 167–176, Pittsburgh, 1992.             
  BibTeX

  @inproceedings{GrMc92a,
       author = {E. Grädel and G. McColm},
       title = {Hierarchies in Transitive Closure Logic, Stratified Datalog and Infinitary Logic},
       booktitle = {Proceedings of 33rd Annual IEEE Symposium on Foundations of Computer Science FOCS `92},
       address = {Pittsburgh},
       year = {1992},
       pages = {167–176},
       note = {See also: journal version \citeGrMc96},
  }
  

• M. Otto. Automorphism Properties of Stationary Logic. Journal of Symbolic Logic, vol. 57, pp. 231–237, 1992.             
  BibTeX

  @article{Ot92,
       author = {M. Otto},
       title = {Automorphism Properties of Stationary Logic},
       journal = {Journal of Symbolic Logic},
       volume = {57},
       year = {1992},
       pages = {231–237},
  }
  

• M. Otto. EM Functors for a Class of Generalized Quantifiers. Archive for Mathematical Logic, vol. 31, pp. 355–371, 1992.             
  BibTeX

  @article{Ot92b,
       author = {M. Otto},
       title = {EM Functors for a Class of Generalized Quantifiers},
       journal = {Archive for Mathematical Logic},
       volume = {31},
       year = {1992},
       pages = {355–371},
  }
  

1991

• E. Grädel. Simple Sentences that are Hard to Decide. Information and Computation, vol. 94, pp. 62–82, 1991.             
  BibTeX

  @article{Gr91,
       author = {E. Grädel},
       title = {Simple Sentences that are Hard to Decide},
       journal = {Information and Computation},
       volume = {94},
       year = {1991},
       pages = {62–82},
  }
  

• E. Grädel. The Expressive Power of Second Order Horn Logic. In Proceedings of 8th Symposium on Theoretical Aspects of Computer Science STACS `91, Hamburg 1991, vol. 480 of LNCS, pp. 466–477. Springer-Verlag, 1991.             
  BibTeX

  @inproceedings{Gr91b,
       author = {E. Grädel},
       title = {The Expressive Power of Second Order Horn Logic},
       booktitle = {Proceedings of 8th Symposium on Theoretical Aspects of Computer Science STACS `91, Hamburg 1991},
       publisher = {Springer-Verlag},
       series = {LNCS},
       volume = {480},
       year = {1991},
       pages = {466–477},
  }
  

• E. Grädel. Capturing Complexity Classes by Fragments of Second Order Logic. In Proceedings of 6th IEEE Conference on Structure in Complexity Theory, pp. 341–352, 1991.             
  BibTeX

  @inproceedings{Gr91c,
       author = {E. Grädel},
       title = {Capturing Complexity Classes by Fragments of Second Order Logic},
       booktitle = {Proceedings of 6th IEEE Conference on Structure in Complexity Theory},
       year = {1991},
       pages = {341–352},
  }
  

• J. Tyszkiewicz. Infinitary Queries and Their Asymptotic Probabilities I: Properties Definable in Transitive Closure Logic. In Proceedings of Workshop on Computer Science Logic CSL `91, vol. 626 of LNCS, pp. 396–410. Springer-Verlag, 1991.                                 
  Abstract   BibTeX

  We present new general method for proving that for certain classes of finite structures the limit law fails for properties expressible in transitive closure logic. In all such cases also all associated asymptotic problems are undecidable.

  @inproceedings{Ty91,
       author = {J. Tyszkiewicz},
       title = {Infinitary Queries and Their Asymptotic Probabilities I: Properties Definable in Transitive Closure Logic},
       booktitle = {Proceedings of Workshop on Computer Science Logic CSL `91},
       publisher = {Springer-Verlag},
       series = {LNCS},
       volume = {626},
       year = {1991},
       pages = {396–410},
       url = {http://www.logic.rwth-aachen.de/pub/jurek/tc.ps},
       copyright = {(c) Springer-Verlag},
  }
  

1990

• J. Duparc. A hierarchy of Context-free $\omega$-languages. Theoretical Computer Science, 1990.                                 
  Abstract   BibTeX

  Twenty years ago, Klaus. W. Wagner came up with a hierarchy of $\omega$-regular sets that actually bares his name. It turned out to be exactly the Wadge hierarchy of the sets of $\omega$-words recognized by Deterministic Finite Automata. We describe the Wadge hierarchy of context-free $\omega$-languages, which stands as an extension of Wagner's work from Automata to Pushdown Automata.

  @article{JDtcs2,
       author = {J. Duparc},
       title = {A hierarchy of Context-free $\omega$-languages},
       journal = {Theoretical Computer Science},
       note = {To appear},
       year = {1990},
       url = {http://www.logic.rwth-aachen.de/pub/duparc/tcs2.ps},
  }
  

• E. Grädel. On Solvable Cases of Hilbert's `Entscheidungsproblem'. 1990.             
  BibTeX

  @misc{Gr90,
       author = {E. Grädel},
       title = {On Solvable Cases of Hilbert's `Entscheidungsproblem'},
       note = {Habilitationsschrift Universität Basel},
       month = {December},
       year = {1990},
  }
  

• E. Grädel. On the Notion of Linear Time Computability. International Journal of Foundations of Computer Science, vol. 1, pp. 295–307, 1990.             
  BibTeX

  @article{Gr90b,
       author = {E. Grädel},
       title = {On the Notion of Linear Time Computability},
       journal = {International Journal of Foundations of Computer Science},
       volume = {1},
       year = {1990},
       pages = {295–307},
       note = {See also: conference version \citeGr89d},
  }
  

• E. Grädel. Satisfiability of Formulae with one $\forall$ is Decidable in Exponential Time. Archive for Mathematical Logic, vol. 29, pp. 256–276, 1990.             
  BibTeX

  @article{Gr90c,
       author = {E. Grädel},
       title = {Satisfiability of Formulae with one $\forall$ is Decidable in Exponential Time},
       journal = {Archive for Mathematical Logic},
       volume = {29},
       year = {1990},
       pages = {256–276},
  }
  

• E. Grädel. Simple Interpretations among Complicated Theories. Information Processing Letters, vol. 35, pp. 235–238, 1990.             
  BibTeX

  @article{Gr90d,
       author = {E. Grädel},
       title = {Simple Interpretations among Complicated Theories},
       journal = {Information Processing Letters},
       volume = {35},
       year = {1990},
       pages = {235–238},
  }
  

• E. Grädel. Domino Games and Complexity. SIAM Journal on Computing, vol. 19, pp. 787–804, 1990.             
  BibTeX

  @article{Gr90e,
       author = {E. Grädel},
       title = {Domino Games and Complexity},
       journal = {SIAM Journal on Computing},
       volume = {19},
       year = {1990},
       pages = {787–804},
  }
  

• M. Otto. Ehrenfeucht-Mostowski Konstruktionen in Erweiterungslogiken. PhD thesis, Freiburg University, 1990.             
  BibTeX

  @phdthesis{Ot90,
       author = {M. Otto},
       title = {Ehrenfeucht-Mostowski Konstruktionen in Erweiterungslogiken},
       school = {Freiburg University},
       year = {1990},
  }
  

1989

• E. Grädel. Dominoes and the Complexity of Subclasses of Logical Theories. Annals of Pure and Applied Logic, vol. 43, pp. 1–30, 1989.             
  BibTeX

  @article{Gr89,
       author = {E. Grädel},
       title = {Dominoes and the Complexity of Subclasses of Logical Theories},
       journal = {Annals of Pure and Applied Logic},
       volume = {43},
       year = {1989},
       pages = {1–30},
  }
  

• E. Grädel. Complexity of Formula Classes in First Order Logic with Functions. In Proceedings of International Conference on Fundamentals of Computation Theory FCT `89, Szeged 1989, vol. 380 of LNCS, pp. 224–233. Springer-Verlag, 1989.             
  BibTeX

  @inproceedings{Gr89b,
       author = {E. Grädel},
       title = {Complexity of Formula Classes in First Order Logic with Functions},
       booktitle = {Proceedings of International Conference on Fundamentals of Computation Theory FCT `89, Szeged 1989},
       publisher = {Springer-Verlag},
       series = {LNCS},
       volume = {380},
       year = {1989},
       pages = {224–233},
  }
  

• E. Grädel. On logical descriptions of some concepts in structural complexity theory. In Proceedings of 3rd Workshop on Computer Science Logic CSL `89, Kaiserslautern, 1989.             
  BibTeX

  @inproceedings{Gr89c,
       author = {E. Grädel},
       title = {On logical descriptions of some concepts in structural complexity theory},
       booktitle = {Proceedings of 3rd Workshop on Computer Science Logic CSL `89},
       address = {Kaiserslautern},
       year = {1989},
  }
  

• E. Grädel. On the Notion of Linear Time Computability. In Proceedings of 3rd Italian Conference on Theoretical Computer Science, pp. 323–334, Mantova. World Scientific Publishing Co., 1989.             
  BibTeX

  @inproceedings{Gr89d,
       author = {E. Grädel},
       title = {On the Notion of Linear Time Computability},
       booktitle = {Proceedings of 3rd Italian Conference on Theoretical Computer Science},
       publisher = {World Scientific Publishing Co.},
       address = {Mantova},
       year = {1989},
       pages = {323–334},
       note = {See also: journal version \citeGr90b},
  }
  

1988

• E. Grädel. Subclasses of Presburger Arithmetic and the Polynomial-Time Hierarchy. Theoretical Computer Science, vol. 56, pp. 289–301, 1988.             
  BibTeX

  @article{Gr88b,
       author = {E. Grädel},
       title = {Subclasses of Presburger Arithmetic and the Polynomial-Time Hierarchy},
       journal = {Theoretical Computer Science},
       volume = {56},
       year = {1988},
       pages = {289–301},
  }
  

• E. Grädel. Domino-Games, with an Application to the Complexity of Boolean Algebras with Bounded Quantifier Alternation. In Proceedings of 5th Annual Symposium on Theoretical Aspects of Computer Science STACS `88, Bordeaux 1988, vol. 294 of LNCS, pp. 98–107. Springer-Verlag, 1988.             
  BibTeX

  @inproceedings{Gr88c,
       author = {E. Grädel},
       title = {Domino-Games, with an Application to the Complexity of Boolean Algebras with Bounded Quantifier Alternation},
       booktitle = {Proceedings of 5th Annual Symposium on Theoretical Aspects of Computer Science STACS `88, Bordeaux 1988},
       publisher = {Springer-Verlag},
       series = {LNCS},
       volume = {294},
       year = {1988},
       pages = {98–107},
  }
  

• E. Grädel. Size of Models versus Length of Computations. On Inseparability by Nondeterministic Time Complexity Classes. In Proceedings of 2nd Workshop on Computer Science Logic CSL `88, Duisburg 1988, vol. 385 of LNCS, pp. 118–137. Springer-Verlag, 1988.             
  BibTeX

  @inproceedings{Gr88d,
       author = {E. Grädel},
       title = {Size of Models versus Length of Computations. On Inseparability by Nondeterministic Time Complexity Classes},
       booktitle = {Proceedings of 2nd Workshop on Computer Science Logic CSL `88, Duisburg 1988},
       publisher = {Springer-Verlag},
       series = {LNCS},
       volume = {385},
       year = {1988},
       pages = {118–137},
  }
  

1987

• E. Grädel. The Complexity of Subclasses of Logical Theories. PhD thesis, Universität Basel, 1987.             
  BibTeX

  @phdthesis{Gr88,
       author = {E. Grädel},
       title = {The Complexity of Subclasses of Logical Theories},
       school = {Universität Basel},
       year = {1987},
       note = {See also: Bulletin of the EATCS 34 (1988), 289-291},
  }
  

• M. Otto. A Reduction Scheme for Phase Spaces with Almost-Kähler Symmetry – Regularity Results for Momentum Level Sets. Journal of Geometry and Physics, vol. 4, pp. 101–118, 1987.             
  BibTeX

  @article{Ot87,
       author = {M. Otto},
       title = {A Reduction Scheme for Phase Spaces with Almost-Kähler Symmetry – Regularity Results for Momentum Level Sets},
       journal = {Journal of Geometry and Physics},
       volume = {4},
       year = {1987},
       pages = {101–118},
  }