Noch nicht erschienen

• 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. To appear.                                 
  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},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/csl08.pdf},
       optyear = {2008},
       note = {to appear},
  }
  

• 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. 5 of Texts in Logic and Games. Amsterdam University Press. To appear.                                 
  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 = {5},
       publisher = {Amsterdam University Press},
       url = {http://www.logic.rwth-aachen.de/~ummels/knaw07.pdf},
       note = {To appear},
  }
  

2008

• 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},
       url = {http://www.logic.rwth-aachen.de/~kaiser/quantitative_games.pdf},
       pages = {301–312},
       year = {2008},
  }
  

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},
  }
  

• 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

• 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},
  }
  

2005

• 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},
  }
  

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},
  }
  

2003

• 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},
  }
  

• 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},
  }
  

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 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},
  }
  

• 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/},
  }
  

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},
  }
  

• 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},
  }
  

• 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},
  }
  

2000

• 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},
  }
  

• 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},
  }
  

1999

• 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},
  }
  

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},
  }
  

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},
  }
  

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},
  }
  

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},
  }
  

• 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},
  }
  

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},
  }
  

• 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},
  }
  

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 wi