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, 2006.             
  BibTeX

  @inproceedings{BDHK06,
       author = {Dietmar Berwanger and Anuj Dawar and Paul Hunter and Stephan Kreutzer},
       booktitle = {{Proceedings of the 23rd Annual Symposium on Theoretical Aspects of Computer Science, STACS 2006}},
       pages = {524--536},
       publisher = {{Springer}},
       series = {{LNCS}},
       title = {{DAG-width and parity games}},
       url = {http://www.logic.rwth-aachen.de/~dwb/pub/dagwidth.pdf},
       volume = {3884},
       year = {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{\"a}del and Stephan Kreutzer},
       journal = {Theoretical Computer Science},
       pages = {174--187},
       title = {{Backtracking Games and Inflationary Fixed Points}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/DaGrKr-tcs05.ps},
       volume = {350},
       year = {2006},
  }
  

2005

• 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},
       journal = {Journal of Logic and Computation},
       pages = {59--74},
       title = {{An Extension to {M}uchnik's Theorem}},
       url = {http://www.mathematik.tu-darmstadt.de/~blumensath/Publications/Muchnik.pdf},
       volume = {15},
       year = {2005},
  }
  

2004

• 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{\"a}del and Stephan Kreutzer},
       journal = {ACM Transations on Computational Logic},
       pages = {282 -- 315},
       title = {{Inflationary fixed points in modal logic}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/DGK-tocl.ps},
       volume = {5},
       year = {2004},
  }
  

• 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, 2004.             
  BibTeX

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

2003

• 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{\"a}del and Stephan Kreutzer},
       booktitle = {{Proceedings of 18th IEEE Symposium on Logic in Computer Science (LICS)}},
       pages = {158 -- 167},
       title = {{Will Deflation Lead to Depletion? {O}n Non-Monotone Fixed Point Inductions.}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/GrKr-lics03.ps},
       year = {2003},
  }
  

• 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},
       booktitle = {{Ausgezeichnete {I}nformatikdissertationen 2002}},
       editor = {Dorothea Wagner and Others},
       pages = {59--68},
       publisher = {German Informatics Society},
       series = {{Lecture Notes in Informatics -- Dissertations}},
       title = {{Pure and Applied Fixed-Point Logics}},
       volume = {D-3},
       year = {2003},
  }
  

2002

• 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},
       booktitle = {{Foundations of Software Technology and Theoretical Computer Science}},
       title = {{Generalising Automaticity to Modal Properties of Finite Structures}},
       url = {http://www.logic.rwth-aachen.de/pub/kreutzer/fsttcs.ps},
       year = {2002},
  }
  

• 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 = {Stephan Kreutzer},
       booktitle = {{Proceedings of the 17th IEEE Symp. on Logic in Computer Science (LICS)}},
       title = {{Expressive Equivalence of Least and Inflationary Fixed-Point Logic}},
       url = {http://www.logic.rwth-aachen.de/pub/kreutzer/ifp.ps},
       year = {2002},
  }
  

• 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 = {Stephan Kreutzer},
       booktitle = {{Annual Conference of the European Association for Computer Science Logic (CSL)}},
       publisher = {Springer},
       series = {{Lecture Notes in Computer Science (LNCS)}},
       title = {{Partial Fixed-Point Logic on Infinite Structures}},
       volume = {2471},
       year = {2002},
  }
  

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

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

2001

• 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, 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 = {Anuj Dawar and Erich Gr{\"a}del and Stephan Kreutzer},
       booktitle = {{Proceedings of 15th Annual Conference of the European Association for Computer Science Logic CSL 2001}},
       publisher = {{Springer}},
       series = {{LNCS}},
       title = {{Inflationary Fixed Points in Modal Logic}},
       url = {http://www.logic.rwth-aachen.de/pub/kreutzer/csl01.ps},
       year = {2001},
  }
  

• 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, 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 = {Stephan Kreutzer},
       booktitle = {{Proceedings of the 8th International Conference on Database Theory (ICDT)}},
       pages = {248--262},
       publisher = {{Springer}},
       series = {{LNCS}},
       title = {{Query Languages for Constraint Databases: First-Order Logic, Fixed-Points, and Convex Hulls}},
       url = {http://www.logic.rwth-aachen.de/pub/kreutzer/icdt2001.ps},
       volume = {1973},
       year = {2001},
  }
  

• 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, 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 = {Stephan Kreutzer},
       booktitle = {{Proceedings of the 8th International Conference on Logic for Programming and Automated Reasoning, {LPAR} 2001, Havana}},
       pages = {465--479},
       publisher = {{Springer}},
       series = {{LNCS}},
       title = {{Operational Semantics for Fixed-Point Logics on Constraint Databases}},
       url = {http://www.logic.rwth-aachen.de/pub/kreutzer/lpar01.ps},
       volume = {2250},
       year = {2001},
  }
  

2000

• 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 = {Stephan Kreutzer},
       booktitle = {{Proceedings of the 19th ACM Symp. on Principles of Database Systems (PODS), 2000}},
       pages = {116--125},
       publisher = {ACM press},
       title = {{Fixed-point Query Languages for Linear Constraint Databases}},
       url = {http://www.logic.rwth-aachen.de/pub/kreutzer/pods00.ps},
       year = {2000},
  }
  

1999

• 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, 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 = {Erich Gr{\"a}del and Stephan Kreutzer},
       booktitle = {{Proceedings of the Annual Conference of the European Association for Computer Science Logic, CSL `99, Madrid}},
       pages = {67--81},
       publisher = {{Springer}},
       series = {{LNCS}},
       title = {{Descriptive Complexity Theory for Constraint Databases}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/GrKr-csl99.ps},
       volume = {1683},
       year = {1999},
  }
  

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

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