2024

• S. Brinke, E. Grädel, L. Mrkonjić, and M. Naaf. Semiring Provenance in the Infinite. In The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen (A. Amarilli and A. Deutsch, Eds.), vol. 119 of Open Access Series in Informatics (OASIcs), pp. 3:1–3:26, Dagstuhl, Germany. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2024.             
  BibTeX

  @inproceedings{BGMN24,
       author = {Sophie Brinke and Erich Gr{\"a}del and Lovro Mrkonji{\'c} and Matthias Naaf},
       title = {Semiring Provenance in the Infinite},
       booktitle = {The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen},
       pages = {3:1--3:26},
       series = {Open Access Series in Informatics (OASIcs)},
       isbn = {978-3-95977-320-1},
       issn = {2190-6807},
       year = {2024},
       volume = {119},
       editor = {Antoine Amarilli and Alin Deutsch},
       publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
       address = {Dagstuhl, Germany},
       url = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Tannen.3},
       doi = {10.4230/OASIcs.Tannen.3},
  }
  

• S. Brinke, E. Grädel, and L. Mrkonjić. Ehrenfeucht-Fraïssé Games in Semiring Semantics. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024) (A. Murano and A. Silva, Eds.), vol. 288 of Leibniz International Proceedings in Informatics (LIPIcs), pp. 19:1–19:22, Dagstuhl, Germany. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2024.             
  BibTeX

  @inproceedings{BGM24,
       author = {Sophie Brinke and Erich Gr{\"a}del and Lovro Mrkonji{\'c}},
       title = {{Ehrenfeucht-Fra{\"i}ss{\'e} Games in Semiring Semantics}},
       booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
       pages = {19:1--19:22},
       series = {Leibniz International Proceedings in Informatics (LIPIcs)},
       isbn = {978-3-95977-310-2},
       issn = {1868-8969},
       year = {2024},
       volume = {288},
       editor = {Aniello Murano and Alexandra Silva},
       publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
       address = {Dagstuhl, Germany},
       url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.19},
       urn = {urn:nbn:de:0030-drops-196623},
       doi = {10.4230/LIPIcs.CSL.2024.19},
       annote = {Keywords: Semiring semantics, elementary equivalence, Ehrenfeucht-Fra\"{i}ss\'{e} games},
  }
  

• E. Grädel, N. Lücking, and M. Naaf. Semiring Provenance for Büchi Games: Strategy Analysis with Absorptive Polynomials. Logical Methods in Computer Science, vol. 20(1), 2024.             
  BibTeX

  @article{GLN24,
       author = {Erich Gr{\"a}del and Niels L{\"u}cking and Matthias Naaf},
       title = {{Semiring Provenance for B{\"u}chi Games: Strategy Analysis with Absorptive Polynomials}},
       url = {https://lmcs.episciences.org/13205},
       doi = {10.46298/lmcs-20(1:21)2024},
       journal = {Logical Methods in Computer Science},
       volume = {20},
       number = {1},
       year = {2024},
  }
  

2023

• C. Bizière, E. Grädel, and M. Naaf. Locality Theorems in Semiring Semantics. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023) (J. Leroux, S. Lombardy, and D. Peleg, Eds.), vol. 272 of Leibniz International Proceedings in Informatics (LIPIcs), pp. 20:1–20:15, Dagstuhl, Germany. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023.             
  BibTeX

  @inproceedings{BGN23b,
       author = {Clotilde Bizi{\`e}re and Erich Gr{\"a}del and Matthias Naaf},
       title = {{Locality Theorems in Semiring Semantics}},
       booktitle = {48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)},
       pages = {20:1--20:15},
       series = {Leibniz International Proceedings in Informatics (LIPIcs)},
       isbn = {978-3-95977-292-1},
       issn = {1868-8969},
       year = {2023},
       volume = {272},
       editor = {J{\'e}r{\^o}me Leroux and Sylvain Lombardy and David Peleg},
       publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
       address = {Dagstuhl, Germany},
       url = {https://drops.dagstuhl.de/opus/volltexte/2023/18554},
       urn = {urn:nbn:de:0030-drops-185546},
       doi = {10.4230/LIPIcs.MFCS.2023.20},
       annote = {Keywords: Semiring semantics, Locality, First-order logic},
  }
  

• C. Bizière, E. Grädel, and M. Naaf. Locality Theorems in Semiring Semantics. arXiv:2303.12627 [cs.LO], full version of MFCS'23 paper, 2023.             
  BibTeX

  @misc{BGN23,
       title = {Locality Theorems in Semiring Semantics},
       author = {Clotilde Bizière and Erich Gr{\"a}del and Matthias Naaf},
       year = {2023},
       howpublished = {arXiv:2303.12627 [cs.LO], full version of MFCS'23 paper},
       url = {http://arxiv.org/abs/2303.12627},
  }
  

• S. Brinke, E. Grädel, and L. Mrkonjić. Ehrenfeucht-Fraïssé Games in Semiring Semantics. arXiv:2308.04910 [cs.LO], full version of CSL'24 paper, 2023.             
  BibTeX

  @misc{BGM23,
       title = {Ehrenfeucht-Fra{\"i}ss{\'e} Games in Semiring Semantics},
       author = {Sophie Brinke and Erich Gr{\"a}del and Lovro Mrkonji{\'c}},
       year = {2023},
       howpublished = {arXiv:2308.04910 [cs.LO], full version of CSL'24 paper},
       url = {http://arxiv.org/abs/2308.04910},
  }
  

2022

• R. Albert and E. Grädel. Unifying hidden-variable problems from quantum mechanics by logics of dependence and independence. Annals of Pure and Applied Logic, vol. 173(10), pp. 103088, 2022.             
  BibTeX

  @article{AG22,
       title = {Unifying hidden-variable problems from quantum mechanics by logics of dependence and independence},
       author = {Rafael Albert and Erich Grädel},
       journal = {Annals of Pure and Applied Logic},
       volume = {173},
       number = {10},
       pages = {103088},
       year = {2022},
       note = {Logics of Dependence and Independence},
       issn = {0168-0072},
       doi = {10.1016/j.apal.2022.103088},
       url = {https://www.sciencedirect.com/science/article/pii/S0168007222000021},
  }
  

• A. Dawar, E. Grädel, and M. Lichter. Limitations of the invertible-map equivalences. Journal of Logic and Computation, 2022.             
  BibTeX

  @article{DGL22,
       author = {Anuj Dawar and Erich Grädel and Moritz Lichter},
       title = {{Limitations of the invertible-map equivalences}},
       journal = {Journal of Logic and Computation},
       year = {2022},
       month = {09},
       issn = {0955-792X},
       doi = {10.1093/logcom/exac058},
       url = {https://academic.oup.com/logcom/advance-article/doi/10.1093/logcom/exac058/6687793?guestAccessKey=7349c158-be02-4116-815a-840ac7880a03},
  }
  

• E. Grädel, H. Helal, M. Naaf, and R. Wilke. Zero-One Laws and Almost Sure Valuations of First-Order Logic in Semiring Semantics. In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2022) (C. Baier and D. Fisman, Eds.), pp. 41:1–41:12. ACM, 2022.             
  BibTeX

  @inproceedings{GHNW22b,
       author = {Erich Gr{\"a}del and Hayyan Helal and Matthias Naaf and Richard Wilke},
       editor = {Christel Baier and Dana Fisman},
       title = {Zero-One Laws and Almost Sure Valuations of First-Order Logic in Semiring Semantics},
       booktitle = {Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2022)},
       pages = {41:1--41:12},
       publisher = {{ACM}},
       year = {2022},
       doi = {10.1145/3531130.3533358},
       url = {https://doi.org/10.1145/3531130.3533358},
  }
  

• E. Grädel, H. Helal, M. Naaf, and R. Wilke. Zero-One Laws and Almost Sure Valuations of First-Order Logic in Semiring Semantics. arXiv:2203.03425 [cs.LO], full version of LICS'22 paper, 2022.             
  BibTeX

  @misc{GHNW22,
       title = {Zero-One Laws and Almost Sure Valuations of First-Order Logic in Semiring Semantics},
       author = {Erich Gr{\"a}del and Hayyan Helal and Matthias Naaf and Richard Wilke},
       year = {2022},
       howpublished = {arXiv:2203.03425 [cs.LO], full version of LICS'22 paper},
       url = {http://arxiv.org/abs/2203.03425},
  }
  

• E. Grädel and R. Wilke. Logics with Multiteam Semantics. ACM Transations on Computational Logic, vol. 23(2), pp. 13:1–13:30, 2022.             
  BibTeX

  @article{GW22,
       author = {Erich Gr{\"a}del and Richard Wilke},
       title = {Logics with Multiteam Semantics},
       journal = {{ACM} Transations on Computational Logic},
       volume = {23},
       number = {2},
       pages = {13:1--13:30},
       year = {2022},
       url = {https://doi.org/10.1145/3487579},
       doi = {10.1145/3487579},
  }
  

• D. Haase, E. Grädel, and R. Wilke. Separation logic and logics with team semantics. Annals of Pure and Applied Logic, vol. 173(10), pp. 103063, 2022.             
  BibTeX

  @article{GHW22,
       title = {Separation logic and logics with team semantics},
       journal = {Annals of Pure and Applied Logic},
       author = {Darion Haase and Erich Gr{\"a}del and Richard Wilke},
       volume = {173},
       number = {10},
       pages = {103063},
       year = {2022},
       note = {Logics of Dependence and Independence},
       issn = {0168-0072},
       doi = {10.1016/j.apal.2021.103063},
       url = {https://www.sciencedirect.com/science/article/pii/S0168007221001214},
  }
  

2021

• R. Albert and E. Grädel. Unifying Hidden-Variable Problems from Quantum Mechanics by Logics of Dependence and Independence. arXiv:2102.10931 [cs.LO], preprint of APAL journal version, 2021.             
  BibTeX

  @misc{AG21,
       title = {Unifying Hidden-Variable Problems from Quantum Mechanics by Logics of Dependence and Independence},
       author = {Rafael Albert and Erich Gr{\"a}del},
       year = {2021},
       howpublished = {arXiv:2102.10931 [cs.LO], preprint of APAL journal version},
       url = {https://arxiv.org/abs/2102.10931},
  }
  

• K. M. Dannert and E. Grädel. Semiring Provenance for Guarded Logics. In Hajnal Andréka and István Németi on Unity of Science: From Computing to Relativity Theory through Algebraic Logic (J. Madarász and G. Székely, Eds.), Outstanding Contribution to Logic, pp. 53–79. Springer, 2021.             
  BibTeX

  @inproceedings{DG21,
       author = {Katrin M. Dannert and Erich Gr{\"{a}}del},
       title = {Semiring Provenance for Guarded Logics},
       booktitle = {Hajnal Andr{\'e}ka and Istv{\'a}n N{\'e}meti on Unity of Science: From Computing to Relativity Theory through Algebraic Logic},
       editor = {Judit Madar{\'a}sz and Gergely Sz{\'e}kely},
       year = {2021},
       series = {Outstanding Contribution to Logic},
       pages = {53--79},
       publisher = {Springer},
       doi = {10.1007/978-3-030-64187-0_3},
       url = {http://www.logic.rwth-aachen.de/pub/DannertGraedel.pdf},
  }
  

• K. M. Dannert, E. Grädel, M. Naaf, and V. Tannen. Semiring Provenance for Fixed-Point Logic. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021) (C. Baier and J. Goubault-Larrecq, Eds.), vol. 183 of Leibniz International Proceedings in Informatics (LIPIcs), pp. 17:1–17:22, Dagstuhl, Germany. Schloss Dagstuhl–Leibniz-Zentrum für Informatik, 2021.             
  BibTeX

  @inproceedings{DGNT21,
       author = {Katrin M. Dannert and Erich Gr{\"a}del and Matthias Naaf and Val Tannen},
       title = {{Semiring Provenance for Fixed-Point Logic}},
       booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
       pages = {17:1--17:22},
       series = {Leibniz International Proceedings in Informatics (LIPIcs)},
       isbn = {978-3-95977-175-7},
       issn = {1868-8969},
       year = {2021},
       volume = {183},
       editor = {Christel Baier and Jean Goubault-Larrecq},
       publisher = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
       address = {Dagstuhl, Germany},
       url = {https://drops.dagstuhl.de/opus/volltexte/2021/13451},
       urn = {urn:nbn:de:0030-drops-134518},
       doi = {10.4230/LIPIcs.CSL.2021.17},
       annote = {Keywords: Finite Model Theory, Semiring Provenance, Absorptive Semirings, Fixed-Point Logics},
  }
  

• A. Dawar, E. Grädel, and M. Lichter. Limitations of the Invertible-Map Equivalences. arXiv:2109.07218 [cs.LO], 2021.             
  BibTeX

  @misc{DGL21,
       title = {Limitations of the Invertible-Map Equivalences},
       author = {Anuj Dawar and Erich Gr{\"a}del and Moritz Lichter},
       year = {2021},
       howpublished = {arXiv:2109.07218 [cs.LO]},
       url = {http://arxiv.org/abs/2109.07218},
  }
  

• E. Grädel, N. Lücking, and M. Naaf. Semiring Provenance for Büchi Games: Strategy Analysis with Absorptive Polynomials. In Proceedings 12th International Symposium on Games, Automata, Logics, and Formal Verification (GandALF 2021) (P. Ganty and D. Bresolin, Eds.), vol. 346 of EPTCS, pp. 67–82, 2021.             
  BibTeX

  @inproceedings{GLN21b,
       author = {Erich Gr{\"a}del and Niels L{\"u}cking and Matthias Naaf},
       editor = {Pierre Ganty and Davide Bresolin},
       title = {Semiring Provenance for B{\"u}chi Games: Strategy Analysis with Absorptive Polynomials},
       booktitle = {Proceedings 12th International Symposium on Games, Automata, Logics, and Formal Verification (GandALF 2021)},
       series = {{EPTCS}},
       volume = {346},
       pages = {67--82},
       year = {2021},
       url = {https://doi.org/10.4204/EPTCS.346.5},
       doi = {10.4204/EPTCS.346.5},
  }
  

• E. Grädel, N. Lücking, and M. Naaf. Semiring Provenance for Büchi Games: Strategy Analysis with Absorptive Polynomials. arXiv:2106.12892 [cs.LO], full version of GandALF'21 paper, 2021.             
  BibTeX

  @misc{GLN21,
       title = {Semiring Provenance for B{\"u}chi Games: Strategy Analysis with Absorptive Polynomials},
       author = {Erich Gr{\"a}del and Niels L{\"u}cking and Matthias Naaf},
       year = {2021},
       howpublished = {arXiv:2106.12892 [cs.LO], full version of GandALF'21 paper},
       url = {http://arxiv.org/abs/2106.12892},
  }
  

• E. Grädel and L. Mrkonjić. Elementary equivalence versus isomorphism in semiring semantics. arXiv:2102.05473 [math.LO], preprint of ICALP'21 paper, 2021.             
  BibTeX

  @misc{GM21,
       title = {Elementary equivalence versus isomorphism in semiring semantics},
       author = {Erich Gr{\"a}del and Lovro Mrkonji{\'c}},
       year = {2021},
       howpublished = {arXiv:2102.05473 [math.LO], preprint of ICALP'21 paper},
       url = {https://arxiv.org/abs/2102.05473},
  }
  

• E. Grädel and L. Mrkonjić. Elementary Equivalence Versus Isomorphism in Semiring Semantics. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021) (N. Bansal, E. Merelli, and J. Worrell, Eds.), vol. 198 of Leibniz International Proceedings in Informatics (LIPIcs), pp. 133:1–133:20, Dagstuhl, Germany. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2021.             
  BibTeX

  @inproceedings{GM21b,
       author = {Erich Gr{\"a}del and Lovro Mrkonji{\'c}},
       title = {{Elementary Equivalence Versus Isomorphism in Semiring Semantics}},
       booktitle = {48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)},
       pages = {133:1--133:20},
       series = {Leibniz International Proceedings in Informatics (LIPIcs)},
       isbn = {978-3-95977-195-5},
       issn = {1868-8969},
       year = {2021},
       volume = {198},
       editor = {Nikhil Bansal and Emanuela Merelli and James Worrell},
       publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
       address = {Dagstuhl, Germany},
       url = {https://drops.dagstuhl.de/opus/volltexte/2021/14202},
       urn = {urn:nbn:de:0030-drops-142022},
       doi = {10.4230/LIPIcs.ICALP.2021.133},
       annote = {Keywords: Semiring semantics, elementary equivalence, axiomatisability},
  }
  

• E. Grädel and P. Pützstück. Logics of dependence and independence: The local variants. Journal of Logic and Computation, vol. 31(7), pp. 1690-1715, 2021.             
  BibTeX

  @article{GP21b,
       author = {Erich Gr{\"a}del and Phil P{\"u}tzst{\"u}ck},
       title = {{Logics of dependence and independence: The local variants}},
       journal = {Journal of Logic and Computation},
       volume = {31},
       number = {7},
       pages = {1690-1715},
       year = {2021},
       month = {07},
       issn = {0955-792X},
       doi = {10.1093/logcom/exab043},
       url = {https://academic.oup.com/logcom/article/31/7/1690/6324789?guestAccessKey=8a5c053c-36b7-497e-a9dd-4ff42b7a9e73},
  }
  

• E. Grädel and P. Pützstück. Logics of Dependence and Independence: The Local Variants. arXiv:2102.10368 [cs.LO], preprint of journal article, 2021.             
  BibTeX

  @misc{GP21,
       title = {Logics of Dependence and Independence: The Local Variants},
       author = {Erich Gr{\"a}del and Phil P{\"u}tzst{\"u}ck},
       year = {2021},
       howpublished = {arXiv:2102.10368 [cs.LO], preprint of journal article},
       url = {https://arxiv.org/abs/2102.10368},
  }
  

2020

• A. Dawar, E. Grädel, and M. Hoelzel. Convergence and Nonconvergence Laws for Random Expansions of Product Structures. In Fields of Logic and Computation III (A. Blass, P. Cégielski, N. Dershowitz, M. Droste, and B. Finkbeiner, Eds.), pp. 118–132. Springer, 2020.             
  BibTeX

  @inproceedings{DGH20,
       author = {Anuj Dawar and Erich Gr{\"a}del and Matthias Hoelzel},
       editor = {Andreas Blass and Patrick C{\'e}gielski and Nachum Dershowitz and Manfred Droste and Bernd Finkbeiner},
       title = {Convergence and Nonconvergence Laws for Random Expansions of Product Structures},
       booktitle = {Fields of Logic and Computation III},
       year = {2020},
       publisher = {Springer},
       pages = {118--132},
       url = {http://www.logic.rwth-aachen.de/pub/DawarGraedelHoelzel.pdf},
       isbn = {978-3-030-48006-6},
       doi = {10.1007/978-3-030-48006-6_9},
  }
  

• E. Grädel. Automatic Structures: Twenty Years Later. In LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020, pp. 21–34. ACM, 2020.             
  BibTeX

  @inproceedings{Graedel20,
       author = {Erich Gr{\"{a}}del},
       title = {Automatic Structures: Twenty Years Later},
       booktitle = {{LICS} '20: 35th Annual {ACM/IEEE} Symposium on Logic in Computer Science, Saarbr{\"{u}}cken, Germany, July 8-11, 2020},
       pages = {21--34},
       publisher = {{ACM}},
       year = {2020},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/lics2020.pdf},
       doi = {10.1145/3373718.3394734},
  }
  

• E. Grädel, D. Haase, and R. Wilke. Separation Logic and Logics with Team Semantics. In Workshop on Logics of Dependence and Independence (J. Väänänen and F. Yang, Eds.), 2020.             
  BibTeX

  @inproceedings{GHW20,
       author = {Erich Gr{\"a}del and Darion Haase and Richard Wilke},
       title = {{Separation Logic and Logics with Team Semantics}},
       year = {2020},
       editor = {J.~V{\"a}{\"a}n{\"a}nen and F.~Yang},
       booktitle = {Workshop on Logics of Dependence and Independence},
       url = {http://www.logic.rwth-aachen.de/pub/wilke/GHW20.pdf},
  }
  

• E. Grädel and M. Otto. Guarded Teams: The Horizontally Guarded Case. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020) (M. Fernández and A. Muscholl, Eds.), vol. 152 of Leibniz International Proceedings in Informatics (LIPIcs), pp. 22:1–22:17, Dagstuhl, Germany. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2020.             
  BibTeX

  @inproceedings{GO20,
       author = {Erich Gr{\"a}del and Martin Otto},
       title = {{Guarded Teams: The Horizontally Guarded Case}},
       booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
       pages = {22:1--22:17},
       series = {Leibniz International Proceedings in Informatics (LIPIcs)},
       isbn = {978-3-95977-132-0},
       issn = {1868-8969},
       year = {2020},
       volume = {152},
       editor = {Maribel Fern{\'a}ndez and Anca Muscholl},
       publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
       address = {Dagstuhl, Germany},
       url = {https://drops.dagstuhl.de/opus/volltexte/2020/11665},
       urn = {urn:nbn:de:0030-drops-116650},
       doi = {10.4230/LIPIcs.CSL.2020.22},
       annote = {Keywords: Team semantics, guarded logics, bisimulation, characterisation theorems},
  }
  

• E. Grädel and V. Tannen. Provenance Analysis for Logic and Games. Moscow Journal of Combinatorics and Number Theory, vol. 9(3), pp. 203–228, 2020.             
  BibTeX

  @article{GT20,
       title = {Provenance Analysis for Logic and Games},
       author = {Erich Gr{\"a}del and Val Tannen},
       journal = {Moscow Journal of Combinatorics and Number Theory},
       volume = {9},
       number = {3},
       pages = {203--228},
       year = {2020},
       publisher = {Mathematical Sciences Publishers},
       doi = {10.2140/moscow.2020.9.203},
       url = {https://doi.org/10.2140/moscow.2020.9.203},
  }
  

• E. Grädel and R. Wilke. Logics with Multiteam Semantics. arXiv:2011.09834 [cs.LO], 2020.             
  BibTeX

  @misc{GW20,
       title = {Logics with Multiteam Semantics},
       author = {Erich Gr{\"a}del and Richard Wilke},
       year = {2020},
       howpublished = {arXiv:2011.09834 [cs.LO]},
       url = {https://arxiv.org/abs/2011.09834},
  }
  

2019

• K. M. Dannert and E. Grädel. Provenance Analysis: A Perspective for Description Logics? In Description Logic, Theory Combination, and All That - Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday, vol. 11560 of Lecture Notes in Computer Science, pp. 266–285. Springer, 2019.             
  BibTeX

  @inproceedings{DBLP:conf/birthday/DannertG19,
       author = {Katrin M. Dannert and Erich Gr{\"{a}}del},
       title = {Provenance Analysis: {A} Perspective for Description Logics?},
       booktitle = {Description Logic, Theory Combination, and All That - Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday},
       pages = {266--285},
       year = {2019},
       series = {Lecture Notes in Computer Science},
       volume = {11560},
       publisher = {Springer},
       url = {http://www.logic.rwth-aachen.de/pub/dannert/ProvenanceAnalysisAPerspective.pdf},
       doi = {10.1007/978-3-030-22102-7\_12},
       timestamp = {Tue, 25 Jun 2019 17:39:16 +0200},
       biburl = {https://dblp.org/rec/bib/conf/birthday/DannertG19},
       bibsource = {dblp computer science bibliography, https://dblp.org},
  }
  

• K. M. Dannert, E. Grädel, M. Naaf, and V. Tannen. Generalized Absorptive Polynomials and Provenance Semantics for Fixed-Point Logic. arXiv:1910.07910 [cs.LO], 2019.             
  BibTeX

  @misc{DGNV19,
       author = {Katrin M. {Dannert} and Erich Gr{\"a}del and Matthias {Naaf} and Val {Tannen}},
       title = {{Generalized Absorptive Polynomials and Provenance Semantics for Fixed-Point Logic}},
       year = {2019},
       url = {http://arxiv.org/abs/1910.07910},
       month = {Oct},
       howpublished = {arXiv:1910.07910 [cs.LO]},
  }
  

• A. Dawar, E. Grädel, and W. Pakusa. Approximations of Isomorphism and Logics with Linear-Algebraic Operators. In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019) (C. Baier, I. Chatzigiannakis, P. Flocchini, and S. Leonardi, Eds.), vol. 132 of Leibniz International Proceedings in Informatics (LIPIcs), pp. 112:1–112:14, Dagstuhl, Germany. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2019.             
  BibTeX

  @inproceedings{dawar_et_al:LIPIcs:2019:10688,
       author = {Anuj Dawar and Erich Gr{\"a}del and Wied Pakusa},
       title = {{Approximations of Isomorphism and Logics with Linear-Algebraic Operators}},
       booktitle = {46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)},
       pages = {112:1--112:14},
       series = {Leibniz International Proceedings in Informatics (LIPIcs)},
       isbn = {978-3-95977-109-2},
       issn = {1868-8969},
       year = {2019},
       volume = {132},
       editor = {Christel Baier and Ioannis Chatzigiannakis and Paola Flocchini and Stefano Leonardi},
       publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
       address = {Dagstuhl, Germany},
       url = {http://drops.dagstuhl.de/opus/volltexte/2019/10688},
       urn = {urn:nbn:de:0030-drops-106887},
       doi = {10.4230/LIPIcs.ICALP.2019.112},
       annote = {Keywords: Finite Model Theory, Graph Isomorphism, Descriptive Complexity, Algebra},
  }
  

• A. Dawar, E. Grädel, and W. Pakusa. Approximations of Isomorphism and Logics with Linear-Algebraic Operators. arXiv:1902.06648 [cs.LO], 2019.             
  BibTeX

  @misc{DGP19,
       title = {Approximations of Isomorphism and Logics with Linear-Algebraic Operators},
       author = {Anuj Dawar and Erich Gr{\"a}del and Wied Pakusa},
       url = {https://arxiv.org/abs/1902.06648},
       howpublished = {arXiv:1902.06648 [cs.LO]},
       year = {2019},
       month = {February},
  }
  

• E. Grädel, M. Grohe, B. Pago, and W. Pakusa. A Finite-Model-Theoretic View on Propositional Proof Complexity. Logical Methods in Computer Science, vol. Volume 15, Issue 1, 2019.             
  BibTeX

  @article{GGPW19,
       title = {{A Finite-Model-Theoretic View on Propositional Proof Complexity}},
       author = {Erich Gr{\"a}del and Martin Grohe and Benedikt Pago and Wied Pakusa},
       url = {https://lmcs.episciences.org/5119},
       doi = {},
       journal = {{Logical Methods in Computer Science}},
       volume = {{Volume 15, Issue 1}},
       year = {2019},
       month = {January},
  }
  

• E. Grädel and W. Pakusa. Rank logic is dead, long live rank logic! The Journal of Symbolic Logic, vol. 84(1), 2019.             
  BibTeX

  @article{GW19,
       title = {{Rank logic is dead, long live rank logic!}},
       author = {Erich Gr{\"a}del and Wied Pakusa},
       url = {https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/rank-logic-is-dead-long-live-rank-logic/F161E336281F2B67E8B3E4CDA5614933},
       doi = {{10.1017/jsl.2018.33}},
       journal = {The Journal of Symbolic Logic},
       volume = {84},
       number = {1},
       publisher = {Cambridge University Press},
       year = {2019},
       month = {March},
  }
  

• E. Grädel and S. Schalthöfer. Choiceless Logarithmic Space. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019) (P. Rossmanith, P. Heggernes, and J. Katoen, Eds.), vol. 138 of Leibniz International Proceedings in Informatics (LIPIcs), pp. 31:1–31:15, Dagstuhl, Germany. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2019.             
  BibTeX

  @inproceedings{GS19,
       author = {Erich Gr{\"a}del and Svenja Schalth{\"o}fer},
       title = {{Choiceless Logarithmic Space}},
       booktitle = {44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
       pages = {31:1--31:15},
       series = {Leibniz International Proceedings in Informatics (LIPIcs)},
       isbn = {978-3-95977-117-7},
       issn = {1868-8969},
       year = {2019},
       volume = {138},
       editor = {Peter Rossmanith and Pinar Heggernes and Joost-Pieter Katoen},
       publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
       address = {Dagstuhl, Germany},
       url = {http://drops.dagstuhl.de/opus/volltexte/2019/10975},
       urn = {urn:nbn:de:0030-drops-109758},
       doi = {10.4230/LIPIcs.MFCS.2019.31},
       annote = {Keywords: Finite Model Theory, Logics for Logspace, Choiceless Computation},
  }
  

2018

• E. Grädel and M. Hoelzel. Dependency Concepts up to Equivalence. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018) (D. Ghica and A. Jung, Eds.), vol. 119 of Leibniz International Proceedings in Informatics (LIPIcs), pp. 25:1–25:21, Dagstuhl, Germany. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2018.             
  BibTeX

  @inproceedings{grdel_et_al:LIPIcs:2018:9692,
       author = {Erich Gr{\"a}del and Matthias Hoelzel},
       title = {{Dependency Concepts up to Equivalence}},
       booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
       pages = {25:1--25:21},
       series = {Leibniz International Proceedings in Informatics (LIPIcs)},
       isbn = {978-3-95977-088-0},
       issn = {1868-8969},
       year = {2018},
       volume = {119},
       editor = {Dan Ghica and Achim Jung},
       publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
       address = {Dagstuhl, Germany},
       url = {http://drops.dagstuhl.de/opus/volltexte/2018/9692},
       urn = {urn:nbn:de:0030-drops-96921},
       doi = {10.4230/LIPIcs.CSL.2018.25},
       annote = {Keywords: Logics of dependence and independence, Team semantics, Existential second-order logic, Observational equivalence, Expressive power},
  }
  

2017

• F. Abu Zaid, A. Dawar, E. Grädel, and W. Pakusa. Definability of Summation Problems for Abelian Groups and Semigroups. In Proceedings of 32th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2017.             
  BibTeX

  @inproceedings{AbuDawGraPak17,
       author = {Faried {Abu Zaid} and Anuj Dawar and Erich Gr{\"a}del and Wied Pakusa},
       title = {{Definability of Summation Problems for Abelian Groups and Semigroups}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/AbuzaidDawGraPak17.pdf},
       booktitle = {{Proceedings of 32th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)}},
       year = {2017},
  }
  

• F. Abu Zaid, E. Grädel, and F. Reinhardt. Advice Automatic Structures and Uniformly Automatic Classes. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017), 2017.             
  BibTeX

  @inproceedings{AbuGraRei17,
       author = {Faried {Abu Zaid} and Erich Gr{\"a}del and Frederic Reinhardt},
       title = {{Advice Automatic Structures and Uniformly Automatic Classes}},
       url = {http://www.logic.rwth-aachen.de/pub/abuzaid/AbuGraRei17.pdf},
       booktitle = {{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}},
       year = {2017},
  }
  

• E. Grädel, B. Pago, and W. Pakusa. The Model-Theoretic Expressiveness of Propositional Proof Systems. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017), 2017.             
  BibTeX

  @inproceedings{GrPaPa17,
       author = {Erich Gr{\"a}del and Benedikt Pago and Wied Pakusa},
       title = {{The Model-Theoretic Expressiveness of Propositional Proof Systems}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/GrPaPa17.pdf},
       booktitle = {{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}},
       year = {2017},
  }
  

• E. Grädel and V. Tannen. Semiring Provenance for First-Order Model Checking. arXiv:1712.01980 [cs.LO], 2017.             
  BibTeX

  @misc{GT17,
       author = {Erich Gr{\"a}del and Val Tannen},
       title = {Semiring Provenance for First-Order Model Checking},
       year = {2017},
       howpublished = {arXiv:1712.01980 [cs.LO]},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/ET17.pdf},
  }
  

2016

• E. Grädel and S. Hegselmann. Counting in Team Semantics. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016) (J. Talbot and L. Regnier, Eds.), vol. 62 of Leibniz International Proceedings in Informatics (LIPIcs), pp. 35:1–35:18, Dagstuhl, Germany. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2016.             
  BibTeX

  @inproceedings{GrHe16,
       author = {Erich Gr{\"a}del and Stefan Hegselmann},
       title = {{Counting in Team Semantics}},
       booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
       pages = {35:1--35:18},
       series = {Leibniz International Proceedings in Informatics (LIPIcs)},
       isbn = {978-3-95977-022-4},
       issn = {1868-8969},
       year = {2016},
       volume = {62},
       editor = {Jean-Marc Talbot and Laurent Regnier},
       publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
       address = {Dagstuhl, Germany},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/GrHe16.pdf},
       urn = {urn:nbn:de:0030-drops-65757},
       doi = {http://dx.doi.org/10.4230/LIPIcs.CSL.2016.35},
       annote = {Keywords: logics with counting, team semantics, fixed-point logic with counting},
  }
  

• E. Grädel. Games for Inclusion Logic and Fixed-Point Logic. In Dependence Logic: Theory and Applications (S. Abramsky et al., Eds.), pp. 73–98. Birkhäuser, 2016.             
  BibTeX

  @inproceedings{Graedel2016,
       author = {Erich Gr{\"{a}}del},
       booktitle = {Dependence Logic: Theory and Applications},
       title = {Games for Inclusion Logic and Fixed-Point Logic},
       editor = {Samson Abramsky and Others},
       year = {2016},
       publisher = {Birkh{\"{a}}user},
       pages = {73--98},
       url = {https://logic.rwth-aachen.de/pub/graedel/dependenceBook.pdf},
  }
  

2015

• F. Canavoi, E. Grädel, S. Lessenich, and W. Pakusa. Defining winning strategies in fixed-point logic. In Proceedings of 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2015.             
  BibTeX

  @inproceedings{CGLP15,
       author = {Felix Canavoi and Erich Gr{\"{a}}del and Simon Lessenich and Wied Pakusa},
       booktitle = {{Proceedings of 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)}},
       title = {{Defining winning strategies in fixed-point logic}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/CGLP15.pdf},
       year = {2015},
  }
  

• E. Grädel and M. Grohe. Is Polynomial Time Choiceless? In Fields of Logic and Computation II. Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday, vol. 9300 of LNCS, pp. 193-209. Springer, 2015.             
  BibTeX

  @inproceedings{GraedelGro15,
       author = {Erich Gr{\"{a}}del and Martin Grohe},
       booktitle = {Fields of Logic and Computation II. Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday},
       title = {{Is Polynomial Time Choiceless?}},
       series = {{LNCS}},
       volume = {9300},
       publisher = {{Springer}},
       pages = {193-209},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/cptYuri.pdf},
       year = {2015},
  }
  

• E. Grädel, Ł. Kaiser, W. Pakusa, and S. Schalthöfer. Characterising Choiceless Polynomial Time with First-Order Interpretations. In Proceedings of 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2015.             
  BibTeX

  @inproceedings{GKPS15,
       author = {Erich Gr{\"{a}}del and \L{}ukasz Kaiser and Wied Pakusa and Svenja Schalth{\"{o}}fer},
       booktitle = {{Proceedings of 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)}},
       title = {{Characterising Choiceless Polynomial Time with First-Order Interpretations}},
       url = {http://www.logic.rwth-aachen.de/pub/schalthoefer/GKPS15.pdf},
       year = {2015},
  }
  

• E. Grädel and W. Pakusa. Rank logic is dead, long live rank logic! CoRR (a conference version appeared in the proceedings of CSL'15), vol. abs/1503.05423, 2015.             
  BibTeX

  @article{GrPa15,
       author = {Erich Gr{\"{a}}del and Wied Pakusa},
       title = {Rank logic is dead, long live rank logic!},
       journal = {CoRR (a conference version appeared in the proceedings of CSL'15)},
       volume = {abs/1503.05423},
       year = {2015},
       url = {http://logic.rwth-aachen.de/pub/pakusa/GrPa15.pdf},
  }
  

2014

• F. Abu Zaid, E. Grädel, M. Grohe, and W. Pakusa. Choiceless Polynomial Time on structures with small Abelian colour classes. In Mathematical Foundations of Computer Science 2014, vol. 8634 of Lecture Notes in Computer Science, pp. 50-62. Springer, 2014.             
  BibTeX

  @incollection{AGGP14,
       author = {Faried {Abu Zaid} and Erich Gr{\"a}del and Martin Grohe and Wied Pakusa},
       title = {{Choiceless Polynomial Time on structures with small Abelian colour classes}},
       url = {http://logic.rwth-aachen.de/pub/pakusa/cptcan.pdf},
       year = {2014},
       booktitle = {Mathematical Foundations of Computer Science 2014},
       volume = {8634},
       series = {Lecture Notes in Computer Science},
       publisher = {Springer},
       pages = {50-62},
  }
  

• F. Abu Zaid, E. Grädel, and S. Jaax. Bisimulation Safe Fixed Point Logic. Advances in Modal Logic, Volume 10, 2014.             
  BibTeX

  @article{AGJ14,
       author = {Faried {Abu Zaid} and Erich Gr{\"a}del and Stefan Jaax},
       title = {Bisimulation Safe Fixed Point Logic},
       journal = {Advances in Modal Logic, Volume 10},
       url = {http://logic.rwth-aachen.de/pub/abuzaid/aiml14.pdf},
       year = {2014},
  }
  

• E. Grädel and M. Otto. The Freedoms of (Guarded) Bisimulation. In Johan van Benthem on Logic and Information Dynamics (A. Baltag and S. Smets, Eds.), vol. 5 of Outstanding Contributions to Logic, pp. 3-31. Springer, 2014.             
  BibTeX

  @incollection{GO14,
       year = {2014},
       booktitle = {Johan van Benthem on Logic and Information Dynamics},
       volume = {5},
       series = {Outstanding Contributions to Logic},
       editor = {Alexandru Baltag and Sonja Smets},
       doi = {10.1007/978-3-319-06025-5_1},
       title = {The Freedoms of (Guarded) Bisimulation},
       url = {http://logic.rwth-aachen.de/pub/graedel/FreedomBisimulation.pdf},
       publisher = {Springer},
       pages = {3-31},
       author = {Erich Gr{\"a}del and Martin Otto},
       language = {English},
  }
  

• F. Canavoi, E. Grädel, and R. Rabinovich. The discrete strategy improvement algorithm for parity games and complexity measures for directed graphs. Theoretical Computer Science, vol. 560, Part 3(0), pp. 235 - 250, 2014.                                 
  Abstract   BibTeX

  Abstract The problem whether winning regions and winning strategies for parity games can be computed in polynomial time is a major open problem in the field of infinite games, which is relevant for many applications in logic and formal verification. For some time the discrete strategy improvement algorithm due to Jurdziński and Vöge had been considered to be a candidate for solving parity games in polynomial time. However, it has recently been proved by Oliver Friedmann that this algorithm requires super-polynomially many iteration steps, for all popular local improvements rules, including switch-all (also with Fearnley's snare memorisation), switch-best, random-facet, random-edge, switch-half, least-recently-considered, and Zadeh's Pivoting rule. We analyse the examples provided by Friedmann in terms of complexity measures for directed graphs such as treewidth, DAG-width, Kelly-width, entanglement, directed pathwidth, and cliquewidth. It is known that for every class of parity games on which one of these parameters is bounded, the winning regions can be efficiently computed. It turns out that with respect to almost all of these measures, the complexity of Friedmann's counterexamples is bounded, and indeed in most cases by very small numbers. This analysis strengthens in some sense Friedmann's results and shows that the discrete strategy improvement algorithm is even more limited than one might have thought. Not only does it require super-polynomial running time in the general case, where the problem of polynomial-time solvability is open, it even has super-polynomial time lower bounds on natural classes of parity games on which efficient algorithms are known.

  @article{CanavoiGraRab14,
       title = {The discrete strategy improvement algorithm for parity games and complexity measures for directed graphs},
       journal = {Theoretical Computer Science},
       volume = {560, Part 3},
       number = {0},
       pages = {235 - 250},
       year = {2014},
       note = {Games, Automata, Logic and Formal Verification},
       issn = {0304-3975},
       doi = {http://dx.doi.org/10.1016/j.tcs.2013.12.021},
       url = {http://logic.rwth-aachen.de/pub/graedel/CanavoiGraRab14.pdf},
       author = {Felix Canavoi and Erich Gr{\"a}del and Roman Rabinovich},
       keywords = {Parity games},
       keywords = {Graph complexity measures},
       keywords = {Treewidth},
  }
  

2013

• F. Abu Zaid, E. Grädel, Ł. Kaiser, and W. Pakusa. Model-Theoretic Properties of omega-Automatic Structures. Theory of Computing Systems, Special Issue dedicated to STACS 2012, 2013.             
  BibTeX

  @article{AGKP12,
       author = {Faried {Abu Zaid} and Erich Gr{\"a}del and \L{}ukasz Kaiser and Wied Pakusa},
       title = {Model-Theoretic Properties of omega-Automatic Structures},
       journal = {Theory of Computing Systems, Special Issue dedicated to STACS 2012},
       url = {http://www.logic.rwth-aachen.de/pub/abuzaid/modelprop.pdf},
       note = {published online 17 October 2013},
       doi = {http://dx.doi.org/10.1007/s00224-013-9508-6},
       year = {2013},
  }
  

• A. Dawar, E. Grädel, B. Holm, E. Kopczynski, and W. Pakusa. Definability of linear equation systems over groups and rings. Logical Methods in Computer Science, Special Issue dedicated to CSL 2012, 2013.             
  BibTeX

  @article{DGHKP13,
       author = {Anuj Dawar and Erich Gr{\"a}del and Bjarki Holm and Eryk Kopczynski and Wied Pakusa},
       title = {{Definability of linear equation systems over groups and rings}},
       journal = {Logical Methods in Computer Science, Special Issue dedicated to CSL 2012},
       url = {http://www.lmcs-online.org/ojs/viewarticle.php?id=1325},
       year = {2013},
  }
  

• E. Grädel. Model-Checking Games for Logics of Incomplete Information. Theoretical Computer Science, Special Issue dedicated to GandALF 2011, pp. 2–14, 2013.             
  BibTeX

  @article{G12,
       author = {Erich Gr{\"a}del},
       journal = {Theoretical Computer Science, Special Issue dedicated to GandALF 2011},
       title = {Model-Checking Games for Logics of Incomplete Information},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/mcgames_journal.pdf},
       year = {2013},
       pages = {2--14},
       doi = {http://dx.doi.org/10.1016/j.tcs.2012.10.033},
  }
  

• E. Grädel and J. Väänänen. Dependence and Independence. Studia Logica, vol. 101(2), pp. 399-410, 2013.             
  BibTeX

  @article{GV10,
       author = {Erich Gr{\"a}del and Jouko V{\"a}{\"a}n{\"a}nen},
       journal = {Studia Logica},
       year = {2013},
       volume = {101},
       title = {{Dependence and Independence}},
       pages = {399-410},
       publisher = {Springer Netherlands},
       number = {2},
       issn = {0039-3215},
       url = {http://dx.doi.org/10.1007/s11225-013-9479-2},
  }
  

2012

• F. Abu Zaid, E. Grädel, and Ł. Kaiser. The Field of Reals is not omega-Automatic. In Proceedings of the 29th International Symposium on Theoretical Aspects of Computer Science, STACS 2012 (C. Dürr and T. Wilke, Eds.), 2012.                                 
  Abstract   BibTeX

  We investigate structural properties of omega-automatic presentations of infinite structures in order to sharpen our methods to determine whether a given structure is omega-automatic. We apply these methods to show that no field of characteristic 0 admits an injective omega-automatic presentation, and that uncountable fields with a definable linear order cannot be omega-automatic.

  @inproceedings{AGK12,
       author = {Faried {Abu Zaid} and Erich Gr{\"a}del and {\L}ukasz Kaiser},
       booktitle = {{Proceedings of the 29th International Symposium on Theoretical Aspects of Computer Science, STACS~2012}},
       editor = {Christoph D{\"u}rr and Thomas Wilke},
       isbn = {978-3-939897-35-4},
       title = {{The Field of Reals is not omega-Automatic}},
       url = {http://www.logic.rwth-aachen.de/pub/abuzaid/reals_not_automatic.pdf},
       year = {2012},
  }
  

• D. Berwanger, E. Grädel, Ł. Kaiser, and R. Rabinovich. Entanglement and the Complexity of Directed Graphs. Theoretical Computer Science, vol. 463(0), pp. 2–25, 2012.                                 
  Abstract   BibTeX

  Entanglement is a parameter for the complexity of finite directed graphs that measures to which extent the cycles of the graph are intertwined. It is defined by way of a game similar in spirit to the cops and robber 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. Entanglement is intimately related with the computational and descriptive complexity of the modal $\mu$-calculus. The number of fixed-point variables needed to describe a finite graph up to bisimulation is captured by its entanglement. This plays a crucial role in the proof that the variable hierarchy of the $\mu$-calculus is strict. We study complexity issues for entanglement and compare it to other structural parameters of directed graphs. One of our main results is 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 a winning strategy. Furthermore, we discuss the case of graphs of entanglement two. While graphs of entanglement zero and one are very simple, graphs of entanglement two allow arbitrary nesting of cycles, and they form a sufficiently rich class for modelling relevant classes of structured systems. We provide characterisations of this class, and propose decomposition notions similar to the ones for tree width, DAG-width, and Kelly-width.

  @article{BGKR12,
       author = {Dietmar Berwanger and Erich Gr{\"a}del and {\L}ukasz Kaiser and Roman Rabinovich},
       journal = {Theoretical Computer Science},
       title = {{Entanglement and the Complexity of Directed Graphs}},
       url = {http://logic.rwth-aachen.de/~rabinovich/entangle.pdf},
       year = {2012},
       volume = {463},
       number = {0},
       pages = {2--25},
       note = {Special Issue on Theory and Applications of Graph Searching Problems},
       issn = {0304-3975},
       doi = {10.1016/j.tcs.2012.07.010},
  }
  

• A. Dawar, E. Grädel, B. Holm, E. Kopczynski, and W. Pakusa. Definability of linear equation systems over groups and rings. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (P. Cégielski and A. Durand, Eds.), vol. 16 of Leibniz International Proceedings in Informatics (LIPIcs), pp. 213–227, Dagstuhl, Germany. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2012.                                 
  Abstract   BibTeX

  Motivated by the quest for a logic for PTIME and recent insights that the descriptive complexity of problems from linear algebra is a crucial aspect of this problem, we study the solvability of linear equation systems over finite groups and rings from the viewpoint of logical (inter-)definability. All problems that we consider are decidable in polynomial time, but not expressible in fixed-point logic with counting. They also provide natural candidates for a separation of polynomial time from rank logics, which extend fixed-point logics by operators for determining the rank of definable matrices and which are sufficient for solvability problems over fields. Based on the structure theory of finite rings, we establish logical reductions among various solvability problems. Our results indicate that all solvability problems for linear equation systems that separate fixed-point logic with counting from PTIME can be reduced to solvability over commutative rings. Further, we prove closure properties for classes of queries that reduce to solvability over rings. As an application, these closure properties provide normal forms for logics extended with solvability operators.

  @inproceedings{DGHKP12,
       author = {Anuj Dawar and Erich Gr{\"a}del and Bjarki Holm and Eryk Kopczynski and Wied Pakusa},
       title = {{Definability of linear equation systems over groups and rings}},
       booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
       pages = {213--227},
       series = {Leibniz International Proceedings in Informatics (LIPIcs)},
       isbn = {978-3-939897-42-2},
       issn = {1868-8969},
       year = {2012},
       volume = {16},
       editor = {Patrick C{\'e}gielski and Arnaud Durand},
       publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
       address = {Dagstuhl, Germany},
       url = {http://drops.dagstuhl.de/opus/volltexte/2012/3674},
       urn = {urn:nbn:de:0030-drops-36749},
       doi = {http://dx.doi.org/10.4230/LIPIcs.CSL.2012.213},
       annote = {Keywords: inite model theory, logics with algebraic operators},
  }
  

• E. Grädel, F. Canavoi, and R. Rabinovich. The discrete strategy improvement algorithm for parity games and complexity measures for directed graphs. In Proceedings of the Third International Symposium on Games, Automata, Logic, and Formal Verification, GandALF 2012 (M. Faella and A. Murano, Eds.), Electronic Proceedings in Theoretical Computer Science, 2012.                                 
  Abstract   BibTeX

  For some time the discrete strategy improvement algorithm due to Jurdziński and V\"oge had been considered as a candidate for solving parity games in polynomial time. However, it has recently been proved by Oliver Friedmann that the strategy improvement algorithm requires super-polynomially many iteration steps, for all popular local improvements rules, including switch-all (also with Fearnley's snare memorisation), switch-best, random-facet, random-edge, switch-half, least-recently-considered, and Zadeh's Pivoting rule. We analyse the examples provided by Friedmann in terms of complexity measures for directed graphs such as treewidth, DAG-width, Kelly-width, entanglement, directed pathwidth, and cliquewidth. It is known that for every class of parity games on which one of these parameters is bounded, the winning regions can be efficiently computed. It turns out that with respect to almost all of these measures, the complexity of Friedmann's counterexamples is bounded, and indeed in most cases by very small numbers. This analysis strengthens in some sense Friedmann's results and shows that the discrete strategy improvement algorithm is even more limited than one might have thought. Not only does it require super-polynomial running time in the general case, where the problem of polynomial-time solvability is open, it even has super-polynomial lower time bounds on natural classes of parity games on which efficient algorithms are known.

  @inproceedings{CGR12,
       author = {Erich Gr{\"a}del and Felix Canavoi and Roman Rabinovich},
       title = {The discrete strategy improvement algorithm for parity games and complexity measures for directed graphs},
       url = {http://www.logic.rwth-aachen.de/~rabinovich/simple_counterexamples.pdf},
       year = {2012},
       booktitle = {Proceedings of the Third International Symposium on Games, Automata, Logic, and Formal Verification, GandALF 2012},
       editor = {Marco Faella and Aniello Murano},
       series = {Electronic Proceedings in Theoretical Computer Science},
       note = {To appear},
  }
  

• E. Grädel and S. Lessenich. Banach-Mazur Games with Simple Winning Strategies. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (P. Cégielski and A. Durand, Eds.), vol. 16 of Leibniz International Proceedings in Informatics (LIPIcs), pp. 305–319, Dagstuhl, Germany. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2012.             
  BibTeX

  @inproceedings{GL12,
       author = {Erich Gr{\"a}del and Simon Lessenich},
       title = {{Banach-Mazur Games with Simple Winning Strategies}},
       booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
       pages = {305--319},
       series = {Leibniz International Proceedings in Informatics (LIPIcs)},
       isbn = {978-3-939897-42-2},
       issn = {1868-8969},
       year = {2012},
       volume = {16},
       editor = {Patrick C{\'e}gielski and Arnaud Durand},
       publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
       address = {Dagstuhl, Germany},
       url = {http://www.logic.rwth-aachen.de/pub/lessenich/BMGamesSimple.pdf},
       urn = {urn:nbn:de:0030-drops-36806},
       doi = {http://dx.doi.org/10.4230/LIPIcs.CSL.2012.305},
       annote = {Keywords: Banach-Mazur games, winning strategies, positional determinacy, Muller winning conditions},
  }
  

• E. Grädel and S. Siebertz. Dynamic Definability. In Proceedings of 15th International Conference on Database Theory, ICDT 2012, 2012.             
  BibTeX

  @inproceedings{GS12,
       author = {Erich Gr{\"a}del and Sebastian Siebertz},
       booktitle = {{Proceedings of 15th International Conference on Database Theory, ICDT~2012}},
       title = {{Dynamic Definability}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/dynamic_definability.pdf},
       year = {2012},
  }
  

• E. Grädel and J. Väänänen. Dependence, Independence, and Incomplete Information. In Proceedings of 15th International Conference on Database Theory, ICDT 2012, 2012.             
  BibTeX

  @inproceedings{GV12,
       author = {Erich Gr{\"a}del and Jouko V{\"a}{\"a}n{\"a}nen},
       booktitle = {{Proceedings of 15th International Conference on Database Theory, ICDT~2012}},
       title = {{Dependence, Independence, and Incomplete Information}},
       url = {http://www.edbt.org/Proceedings/2012-Berlin/papers/keynotes/a1-gradel.pdf},
       year = {2012},
  }
  

2011

• K. Apt and E. Grädel (Eds.). Lectures in Game Theory for Computer Scientists. Cambridge University Press, 2011.                                 
  Abstract   BibTeX

  Games provide mathematical models for interaction. Numerous tasks in computer science can be formulated in game-theoretic terms. This fresh and intuitive way of thinking through complex issues reveals underlying algorithmic questions and clarifies the relationships between different domains. This collection of lectures, by specialists in the field, provides an excellent introduction to various aspects of game theory relevant for applications in computer science that concern program design, synthesis, verification, testing and design of multi-agent or distributed systems. Originally devised for a Spring School organised by the GAMES Networking Programme in 2009, these lectures have since been revised and expanded, and range from tutorials concerning fundamental notions and methods to more advanced presentations of current research topics. This volume is a valuable guide to current research on game-based methods in computer science for undergraduate and graduate students. It will also interest researchers working in mathematical logic, computer science and game theory.

  @book{ApGr11,
       editor = {K. Apt and Erich Gr{\"a}del},
       img = {Bertinoro/foxes\_small.jpg},
       publisher = {Cambridge University Press},
       title = {{Lectures in Game Theory for Computer Scientists}},
       url = {http://www.cambridge.org/gb/knowledge/isbn/item5760379},
       year = {2011},
  }
  

• V. Bárány, E. Grädel, and S. Rubin. Automata-Based Presentations of Infinite Structures. In Finite and Algorithmic Model Theory (J. Esparza, C. Michaux, and C. Steinhorn, Eds.), pp. 1–76, 2011.             
  BibTeX

  @incollection{BGR10,
       author = {Vince B{\'a}r{\'a}ny and Erich Gr{\"a}del and Sasha Rubin},
       booktitle = {{Finite and Algorithmic Model Theory}},
       editor = {Javier Esparza and Christian Michaux and Charles Steinhorn},
       isbn = {9780521718202},
       month = {March},
       pages = {1--76},
       title = {{Automata-Based Presentations of Infinite Structures}},
       url = {http://logic.rwth-aachen.de/pub/graedel/surveyBGR.pdf},
       year = {2011},
  }
  

• E. Grädel. Back and Forth Between Logics and Games. In Lectures in Game Theory for Computer Scientists, pp. 99–145. Springer, 2011.             
  BibTeX

  @incollection{Graedel11,
       author = {Erich Gr{\"a}del},
       booktitle = {{Lectures in Game Theory for Computer Scientists}},
       pages = {99--145},
       publisher = {{Springer}},
       title = {{Back and Forth Between Logics and Games}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/backandforth.pdf},
       year = {2011},
  }
  

2010

• A. Dawar and E. Grädel. Properties of Almost All Graphs and Generalized Quantifiers. Fundamenta Informaticae, vol. 98, pp. 351–372, 2010.                                 
  Abstract   BibTeX

  We study 0-1 laws for extensions of first-order logic by Lindström quantifiers. We state sufficient conditions on a quantifier Q expressing a graph property, for the logic FO[Q] — the extension of first-order logic by means of the quantifier Q — to have a 0-1 law. We use these conditions to show, in particular, that FO[Rig], where Rig is the quantifier expressing rigidity, has a 0-1 law. We also show that extensions of first-order logic with quantifiers for Hamiltonicity, regularity and self-complementarity of graphs do not have a 0-1 law. Blass and Harary pose the question whether there is a logic which is powerful enough to express Hamiltonicity or rigidity and which has a 0-1 law. It is a consequence of our results that there is no such regular logic (in the sense of abstract model theory) in the case of Hamiltonicity, but there is one in the case of rigidity. We also consider sequences of vectorized quantifiers, and show that the extensions of first-order logic obtained by adding such sequences generated by quantifiers that are closed under substructures have 0-1 laws. The positive results also extend to the infinitary logic with finitely many variables.

  @article{DG10,
       author = {Anuj Dawar and Erich Gr{\"a}del},
       journal = {Fundamenta Informaticae},
       pages = {351--372},
       title = {{Properties of Almost All Graphs and Generalized Quantifiers}},
       url = {http://logic.rwth-aachen.de/pub/graedel/DG09-GQfinal.pdf},
       volume = {98},
       year = {2010},
  }
  

• D. Fischer, E. Grädel, and Ł. Kaiser. Model Checking Games for the Quantitative mu-Calculus. Theory Comput. Syst., vol. 47(3), pp. 696–719, 2010.                                 
  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{FGK10,
       author = {Diana Fischer and Erich Gr{\"a}del and {\L}ukasz Kaiser},
       journal = {Theory Comput. Syst.},
       number = {3},
       pages = {696--719},
       title = {{Model Checking Games for the Quantitative mu-Calculus}},
       url = {http://logic.rwth-aachen.de/~kaiser/quantitative_games_journal.pdf},
       volume = {47},
       year = {2010},
  }
  

2009

• E. Grädel and R. Kahle (Eds.). Proceedings of the 18th Annual Conference of the European Association for Computer Science Logic, CSL '09. Springer, 2009.             
  BibTeX

  @proceedings{GR09,
       editor = {Erich Gr{\"a}del and Reinhard Kahle},
       publisher = {{Springer}},
       series = {{LNCS}},
       title = {{Proceedings of the 18th Annual Conference of the European Association for Computer Science Logic, CSL~'09}},
       volume = {5771},
       year = {2009},
  }
  

• E. Grädel, Ł. Kaiser, and R. Rabinovich. Directed Graphs of Entanglement Two. In Proceedings of the 17th International Symposium on Fundamentals of Computation Theory, FCT '09, vol. 5699 of LNCS, pp. 169–181. Springer, 2009.                                 
  Abstract   BibTeX

  Entanglement is a complexity measure for directed graphs that was used to show that the variable hierarchy of the propositional modal $\mu$-calculus is strict. While graphs of entanglement zero and one are indeed very simple, some graphs of entanglement two already contain interesting nesting of cycles. This motivates our study of the class of graphs of entanglement two, as these are both simple in a sense and already complex enough for modelling certain structured systems. Undirected graphs of entanglement two were already studied by Belkhir and Santocanale and a structural decomposition for such graphs was given. We study the general case of directed graphs of entanglement two and prove that they can be decomposed as well, in a way similar to the known decompositions for tree-width, DAG-width and Kelly-width. Moreover, we show that all graphs of entanglement two have both DAG-width and Kelly-width three. Since there exist both graphs with DAG-width three and graphs with Kelly-width three, but with arbitrary high entanglement, this confirms that graphs of entanglement two are a very basic class of graphs with cycles intertwined in an interesting way.

  @inproceedings{GKR09,
       author = {Erich Gr{\"a}del and {\L}ukasz Kaiser and Roman Rabinovich},
       booktitle = {{Proceedings of the 17th International Symposium on Fundamentals of Computation Theory, FCT~'09}},
       pages = {169--181},
       publisher = {{Springer}},
       series = {{LNCS}},
       title = {{Directed Graphs of Entanglement Two}},
       url = {http://logic.rwth-aachen.de/~kaiser/entanglement2.pdf},
       volume = {5699},
       year = {2009},
  }
  

2008

• 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, 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{\"a}del},
       booktitle = {{Proceedings of the 17th Annual Conference on Computer Science Logic, CSL~2008}},
       pages = {354--368},
       publisher = {{Springer}},
       series = {{LNCS}},
       title = {{The Descriptive Complexity of Parity Games}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/csl08.pdf},
       volume = {5213},
       year = {2008},
  }
  

• D. Fischer, E. Grädel, and Ł. Kaiser. Model Checking Games for the Quantitative μ-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{\"a}del and {\L}ukasz Kaiser},
       booktitle = {{Proceedings of the 25th International Symposium on Theoretical Aspects of Computer Science, STACS~2008}},
       editor = {Susanne Albers and Pascal Weil},
       pages = {301--312},
       title = {{Model Checking Games for the Quantitative $\mu$-Calculus}},
       year = {2008},
  }
  

• 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,
       address = {Dagstuhl, Germany},
       annote = {Keywords: Games, strategies, determinacy, positional determinacy, definability, complexity},
       author = {Erich Gr{\"a}del},
       booktitle = {{Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS~2008}},
       editor = {Ramesh Hariharan and Madhavan Mukund and V. Vinay},
       publisher = {Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik, Germany},
       title = {{{B}anach-{M}azur Games on Graphs}},
       url = {http://drops.dagstuhl.de/opus/volltexte/2008/1768},
       year = {2008},
  }
  

• 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{\"a}del and Michael Ummels},
       booktitle = {{New Perspectives on Games and Interaction}},
       editor = {Krzysztof Apt and Robert van Rooij},
       pages = {151--178},
       publisher = {Amsterdam University Press},
       series = {{Texts in Logic and Games}},
       title = {{Solution Concepts and Algorithms for Infinite Multiplayer Games}},
       url = {http://www.logic.rwth-aachen.de/~ummels/knaw07.pdf},
       volume = {4},
       year = {2008},
  }
  

2007

• D. Berwanger, E. Grädel, and G. Lenzi. The variable hierarchy of the μ-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{\"a}del and Giacomo Lenzi},
       journal = {Theory of Computing Systems},
       pages = {437--466},
       title = {{The variable hierarchy of the $\mu$-calculus is strict}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/BeGrLe-tocs07.pdf},
       volume = {40},
       year = {2007},
  }
  

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

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

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

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

• 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, pp. 89–116. 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{\"a}del and {\L}ukasz Kaiser},
       booktitle = {{Interactive Logic}},
       editor = {Johan van Benthem and Benedikt L{\"o}we and Dov Gabbay},
       pages = {89--116},
       publisher = {Amsterdam University Press},
       series = {{Texts in Logic and Games}},
       title = {{What kind of memory is needed to win infinitary Muller games?}},
       url = {http://www.logic.rwth-aachen.de/pub/kaiser/memory_kinds.pdf},
       volume = {1},
       year = {2007},
  }
  

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

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

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

• 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 = {Erich Gr{\"a}del and Igor Walukiewicz},
       journal = {Logical Methods in Computer Science},
       title = {{Positional Determinacy of Games with Infinitely Many Priorities}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/GrWa-lmcs06.pdf},
       year = {2006},
  }
  

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, 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{\"a}del},
       booktitle = {{Proceedings of LPAR 2004, Montevideo, Uruguay}},
       pages = {209--223},
       publisher = {{Springer}},
       series = {{LNCS}},
       task = {2},
       title = {{Entanglement -- {A} Measure for the Complexity of Directed Graphs with Applications to Logic and Games}},
       url = {http://www.logic.rwth-aachen.de/pub/dwb/BG_lpar04.pdf},
       volume = {3452},
       year = {2005},
  }
  

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{\"a}del},
       journal = {Theory of Computing Systems},
       pages = {675--694},
       publisher = {{Springer}},
       task = {2,7},
       title = {{Fixed-Point Logics and Solitaire Games}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/BeGr_tocs.pdf},
       volume = {37},
       year = {2004},
  }
  

• 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{\"a}del},
       journal = {Theory of Computing Systems},
       pages = {641 -- 674},
       publisher = {{Springer}},
       title = {{Finite Presentations of Infinite Structures: Automata and Interpretations}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/BlGr_tocs.pdf},
       volume = {37},
       year = {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},
  }
  

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

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

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, 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{\"a}del and Sthephan Kreutzer},
       booktitle = {{Proceedings of the 10th International Conference on Logic for Programming and Automated Reasoning}},
       pages = {226--240},
       publisher = {{Springer}},
       series = {{LNCS}},
       task = {7},
       title = {{Once Upon a Time in the West. {D}eterminacy, Complexity and Definability of Path Games.}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/lpar03.ps},
       volume = {2850},
       year = {2003},
  }
  

• 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 = {Erich Gr{\"a}del},
       booktitle = {{Proceedings of Kalm{\'a}r Workshop on Logic and Computer Science, Szeged}},
       title = {{Decidable fragments of first-order and fixed-point logic. {F}rom prefix-vocabulary classes to guarded logics.}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/Gr-kalmar03.ps},
       year = {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},
  }
  

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

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

2002

• 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{\"a}del},
       booktitle = {{Proceedings of the 2nd International Workshop on Complexity in Automated Deduction, CiAD 2002}},
       note = {Submitted to ACM Theory of Computing Systems},
       title = {{Finite Presentations of Infinite Structures}},
       url = {http://www.logic.rwth-aachen.de/pub/blume/tocs-2002-ciad.ps},
       year = {2002},
  }
  

• 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 = {Georg Gottlob and Erich Gr{\"a}del and H.~Veith},
       journal = {ACM Transactions on Computational Logic},
       number = {1},
       pages = {1--35},
       title = {{Datalog {LITE}: {A} deductive query language with linear time model checking}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/GoGrVe-tocl02.ps},
       volume = {3},
       year = {2002},
  }
  

• 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 = {Erich Gr{\"a}del},
       journal = {Theoretical Computer Science},
       pages = {129--152},
       title = {{Guarded fixed point logic and the monadic theory of trees}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/Gr-tcs01.ps},
       volume = {288},
       year = {2002},
  }
  

• 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 = {Erich Gr{\"a}del},
       booktitle = {{Proceedings of WOLLIC 02}},
       publisher = {Elsevier},
       series = {{Electronic Notes in Theoretical Computer Science}},
       title = {{Model Checking Games}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/Gr-wollic02.ps},
       volume = {67},
       year = {2002},
  }
  

• 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 = {Erich Gr{\"a}del and Colin Hirsch and Martin Otto},
       journal = {ACM Transactions on Computational Logics},
       note = {See also: conference version \cite{GrHiOt00}},
       number = {3},
       pages = {418 -- 463},
       title = {{Back and Forth Between Guarded and Modal Logics}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/GrHiOt-tocl02.ps},
       volume = {3},
       year = {2002},
  }
  

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

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

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, 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 = {Dietmar Berwanger and Erich Gr{\"a}del},
       booktitle = {{Proceedings of the 8th International Conference on Logic for Programming and Automated Reasoning, {LPAR} 2001, Havana}},
       editor = {R. Nieuwenhuis and A. Voronkov},
       publisher = {{Springer}},
       series = {{LNCS}},
       title = {{Games and Model Checking for Guarded Logics}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/lpar.ps},
       volume = {2250},
       year = {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},
  }
  

• 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 = {Erich Gr{\"a}del},
       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},
       title = {{Why are modal logics so robustly decidable?}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/Gr-trends01.ps},
       year = {2001},
  }
  

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 = {Achim Blumensath and Erich Gr{\"a}del},
       booktitle = {{Proceedings of 15th IEEE Symposium on Logic in Computer Science LICS 2000}},
       pages = {51--62},
       title = {{Automatic Structures}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/BlGr-lics00.ps},
       year = {2000},
  }
  

• 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 = {Elisabeth Gon\c{c}alv{\`e}s and Erich Gr{\"a}del},
       booktitle = {{Proceedings of 2000 International Workshop on Description Logics -- DL2000}},
       pages = {123--132},
       title = {{Decidability issues for action guarded logics}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/GoGr-dl00.ps},
       year = {2000},
  }
  

• 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 = {Georg Gottlob and Erich Gr{\"a}del and H.~Veith},
       booktitle = {{Logic-Based Artificial Intelligence}},
       chapter = {19},
       editor = {J. Minker},
       publisher = {Kluwer},
       title = {{Linear Time Datalog for Branching Time Logic}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/GoGrVe-minker00.ps},
       year = {2000},
  }
  

• 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,
       address = {Santa Barbara},
       author = {Erich Gr{\"a}del and Colin Hirsch and Martin Otto},
       booktitle = {{Proceedings of 15th IEEE Symposium on Logic in Computer Science LICS 2000}},
       note = {See also: journal version \cite{GrHiOt00a}},
       pages = {217--228},
       title = {{Back and Forth Between Guarded and Modal Logics}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/GrHiOt-lics00.ps},
       year = {2000},
  }
  

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 = {Erich Gr{\"a}del},
       journal = {Bulletin of the European Association for Theoretical Computer Science},
       pages = {90--103},
       title = {{Why are modal logics so robustly decidable?}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/Gr-eatcs99.ps},
       volume = {68},
       year = {1999},
  }
  

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

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

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

  @article{Gr99d,
       author = {Erich Gr{\"a}del},
       journal = {Journal of Symbolic Logic},
       pages = {1719--1742},
       title = {{On the restraining power of guards}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/Gr-jsl99.ps},
       volume = {64},
       year = {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},
  }
  

• 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 = {Erich Gr{\"a}del and Anders Malmstr{\"o}m},
       journal = {Archive for Mathematical Logic},
       pages = {205--215},
       title = {{0-1 Laws for Recursive Structures}},
       url = {http://www.logic.rwth-aachen.de/pub/anders/recursive.ps},
       volume = {38},
       year = {1999},
  }
  

• 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 = {Erich Gr{\"a}del},
       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},
       title = {{The decidability of guarded fixed point logic}},
       url = {http://turing.wins.uva.nl/~j50/cdrom/contribs/graedel/index.html},
       year = {1999},
  }
  

• 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 = {Erich Gr{\"a}del and Martin Otto},
       journal = {Theoretical Computer Science},
       pages = {73--113},
       title = {{On Logics with Two Variables}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/GrOt-tcs99.ps},
       volume = {224},
       year = {1999},
  }
  

• 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 = {Erich Gr{\"a}del and Martin Otto and Eric Rosen},
       journal = {Archive for Mathematical Logic},
       note = {See also: conference version \cite{GraedelOttoRosen97a}},
       pages = {213--354},
       title = {{Undecidability Results on Two-Variable Logics}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/gor.ps},
       volume = {38},
       year = {1999},
  }
  

• 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 = {Erich Gr{\"a}del and Eric Rosen},
       journal = {Mathematical Logic Quarterly},
       pages = {315--325},
       title = {{Preservation theorems for two-variable logic}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/preservation.ps},
       volume = {45},
       year = {1999},
  }
  

• 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 = {Erich Gr{\"a}del and Eric Rosen},
       booktitle = {{Proceedings of 14th IEEE Symposium on Logic in Computer Science LICS `99, Trento}},
       pages = {14--23},
       title = {{Two-variable descriptions of regularity}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/GrRo-lics99.ps},
       year = {1999},
  }
  

• 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, 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 = {Erich Gr{\"a}del and Marc Spielmann},
       booktitle = {{World Congress on Formal Methods (FM `99)}},
       editor = {J. Wing and J. Woodcock and J. Davies},
       pages = {1738--1757},
       publisher = {{Springer}},
       series = {{LNCS}},
       title = {{Logspace Reducibility via Abstract State Machines}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/GrSp-fm99.ps},
       volume = {1709},
       year = {1999},
  }
  

• 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 = {Erich Gr{\"a}del and Igor Walukiewicz},
       booktitle = {{Proceedings of 14th IEEE Symposium on Logic in Computer Science LICS `99, Trento}},
       pages = {45--54},
       title = {{Guarded Fixed Point Logic}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/GrWa-lics99.ps},
       year = {1999},
  }
  

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,
       address = {Trento},
       author = {Erich Gr{\"a}del},
       booktitle = {{Proceedings of 1998 International Workshop on Description Logics DL {`98}}},
       note = {Extended abstract},
       publisher = {CEUR Electronic Workshop Proceedings},
       title = {{Guarded fragments of first-order logic: a perspective for new description logics?}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/Gr-dl98.ps},
       year = {1998},
  }
  

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

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

• 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 = {Erich Gr{\"a}del and Yuri Gurevich and Colin Hirsch},
       booktitle = {{17th ACM Symposium on Principles of Database Systems PODS `98, Seattle}},
       publisher = {ACM Press},
       title = {{The complexity of query reliability}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/GrGuHi-pods98.ps},
       year = {1998},
  }
  

1997

• 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 = {Erich Gr{\"a}del and Phonion Kolaitis and Moshe Vardi},
       journal = {Bulletin of Symbolic Logic},
       pages = {53--69},
       title = {{On the Decision Problem for Two-Variable First-Order Logic}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/basl.ps},
       volume = {3},
       year = {1997},
  }
  

• 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 = {Erich Gr{\"a}del and Martin Otto and Eric Rosen},
       booktitle = {{Proceedings of 12th IEEE Symposium on Logic in Computer Science LICS `97, Warschau}},
       title = {{Two-Variable Logic with Counting is Decidable}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/gorc2.ps},
       year = {1997},
  }
  

• 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 = {Erich Gr{\"a}del and Martin Otto and Eric Rosen},
       booktitle = {{Proceedings of 14th Symposium on Theoretical Aspects of Computer Science STACS`97}},
       note = {See also: journal version \cite{GraedelOttoRosen98}},
       pages = {249--260},
       series = {{Lecture Notes in Computer Science}},
       title = {{Undecidability Results on Two-Variable Logics}},
       volume = {1200},
       year = {1997},
  }
  

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 Erich Gr{\"a}del},
       journal = {Journal of Computer and System Sciences},
       note = {See also: conference version \cite{CoGr94}},
       pages = {283--297},
       title = {{Logical Definability of Counting Functions}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/counting.ps},
       volume = {53},
       year = {1996},
  }
  

• 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 = {Erich Gr{\"a}del and K.~Meer},
       editor = {J. Renegar and M. Shub and S. Smale},
       journal = {Mathematics of Numerical Analysis: Real Number Algorithms},
       note = {See also: conference version \cite{GrMe95}},
       pages = {381--403},
       series = {{AMS Lectures in Applied Mathematics}},
       title = {{Descriptive Complexity Theory over the Real Numbers}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/GrMe-amsAM96.ps},
       volume = {32},
       year = {1996},
  }
  

• 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 = {Erich Gr{\"a}del and G. McColm},
       journal = {Annals of Pure and Applied Logic},
       note = {See also: conference version \cite{GrMc92a}},
       pages = {166--199},
       title = {{Hierarchies in Transitive Closure Logic, Stratified Datalog and Infinitary Logic}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/GrMcC-apal96.ps},
       volume = {77},
       year = {1996},
  }
  

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 = {Anuj Dawar and Erich Gr{\"a}del},
       booktitle = {{Proceedings of 10th IEEE Symposium on Logic in Computer Science LICS `95, San Diego}},
       pages = {54--64},
       title = {{Generalized Quantifiers and 0-1 Laws}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/lics95.ps},
       year = {1995},
  }
  

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

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

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

  @inproceedings{GrGu95a,
       author = {Erich Gr{\"a}del and Yuri Gurevich},
       booktitle = {{Logic and Computational Complexity, Selected Papers}},
       editor = {D. Leivant},
       note = {See also: journal version \cite{GrGu98}},
       pages = {213--366},
       publisher = {{Springer}},
       title = {{Metafinite Model Theory}},
       year = {1995},
  }
  

• 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,
       address = {Las Vegas},
       author = {Erich Gr{\"a}del and K.~Meer},
       booktitle = {{Proceedings of the 27th ACM-Symposium on Theory of Computing, STOC 95}},
       note = {See also: journal version \cite{GrMe96}},
       title = {{Descriptive Complexity Theory over the Real Numbers}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/stoc95.ps},
       year = {1995},
  }
  

• 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 = {Erich Gr{\"a}del and G. McColm},
       journal = {Information and Computation},
       note = {See also: conference version \cite{GrMc92}},
       pages = {129--135},
       title = {{On the {P}ower of {D}eterministic {T}ransitive {C}losures}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/GrMcC-ic95.ps},
       volume = {119},
       year = {1995},
  }
  

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,
       address = {Amsterdam},
       author = {K. Compton and Erich Gr{\"a}del},
       booktitle = {{Proceedings of 9th IEEE Conference on Structure in Complexity Theory}},
       note = {See also: journal version \cite{CoGr96}},
       pages = {255--266},
       title = {{Logical Definability of Counting Functions}},
       year = {1994},
  }
  

• 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 = {Erich Gr{\"a}del},
       journal = {Methods of Logic in Computer Science},
       pages = {299--314},
       title = {{Definability on Finite Structures and the Existence of One-Way Functions}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/Gr-mlcs94.ps},
       volume = {1},
       year = {1994},
  }
  

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

  @inproceedings{GrGu94,
       author = {Erich Gr{\"a}del and Yuri Gurevich},
       booktitle = {{Proceedings of 21st International Colloquium on Automata, Languages and Programming ICALP 94}},
       note = {See also: journal version \cite{GrGu95}},
       pages = {118--129},
       publisher = {{Springer}},
       series = {{LNCS}},
       title = {{Tailoring Recursion for Complexity}},
       volume = {820},
       year = {1994},
  }
  

• 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, 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 = {Erich Gr{\"a}del and Anders Malmstr{\"o}m},
       booktitle = {{Computer Science Logic, 7th Workshop, CSL `93, Swansea 1993, Selected Papers}},
       editor = {E. B{\"o}rger and Y. Gurevich and K. Meinke},
       pages = {139--149},
       publisher = {{Springer}},
       series = {{LNCS}},
       title = {{Approximable minimization problems and optimal solutions on random input}},
       url = {http://www.logic.rwth-aachen.de/pub/anders/csl93.ps},
       volume = {832},
       year = {1994},
  }
  

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

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

• 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, 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 = {Erich Gr{\"a}del and Martin Otto},
       booktitle = {{Computer Science Logic, 6th Workshop, CSL `92, San Miniato 1992, Selected Papers}},
       editor = {E. B{\"o}rger and G. J{\"a}ger and H. Kleine B{\"u}ning and S. Martini and M. M. Richter},
       pages = {231--247},
       publisher = {{Springer}},
       series = {{LNCS}},
       title = {{Inductive Definability with Counting on Finite Structures}},
       url = {http://www.logic.rwth-aachen.de/pub/otto/CSL92.ps},
       volume = {702},
       year = {1993},
  }
  

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 = {Erich Gr{\"a}del},
       journal = {Theoretical Computer Science},
       pages = {35--57},
       title = {{Capturing Complexity Classes by Fragments of Second Order Logic}},
       volume = {101},
       year = {1992},
  }
  

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

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

• 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,
       address = {Santa Cruz},
       author = {Erich Gr{\"a}del and G. McColm},
       booktitle = {{Proceedings of 7th IEEE Symposium on Logic in Computer Science LICS `92}},
       note = {See also: journal version \cite{GrMc95}},
       pages = {58--63},
       title = {{Deterministic versus Nondeterministic Transitive Closure Logic}},
       year = {1992},
  }
  

• 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,
       address = {Pittsburgh},
       author = {Erich Gr{\"a}del and G. McColm},
       booktitle = {{Proceedings of 33rd Annual IEEE Symposium on Foundations of Computer Science FOCS `92}},
       note = {See also: journal version \cite{GrMc96}},
       pages = {167--176},
       title = {{Hierarchies in Transitive Closure Logic, Stratified Datalog and Infinitary Logic}},
       year = {1992},
  }
  

1991

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

  @article{Gr91,
       author = {Erich Gr{\"a}del},
       journal = {Information and Computation},
       pages = {62--82},
       title = {{Simple Sentences that are Hard to Decide}},
       volume = {94},
       year = {1991},
  }
  

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

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

• 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 = {Erich Gr{\"a}del},
       booktitle = {{Proceedings of 6th IEEE Conference on Structure in Complexity Theory}},
       pages = {341--352},
       title = {{Capturing Complexity Classes by Fragments of Second Order Logic}},
       year = {1991},
  }
  

1990

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

  @misc{Gr90,
       author = {Erich Gr{\"a}del},
       month = {December},
       note = {Habilitationsschrift Universit{\"a}t Basel},
       title = {{On Solvable Cases of Hilbert's `Entscheidungsproblem'}},
       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 = {Erich Gr{\"a}del},
       journal = {International Journal of Foundations of Computer Science},
       note = {See also: conference version \cite{Gr89d}},
       pages = {295--307},
       title = {{On the Notion of Linear Time Computability}},
       volume = {1},
       year = {1990},
  }
  

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

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

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

  @article{Gr90d,
       author = {Erich Gr{\"a}del},
       journal = {Information Processing Letters},
       pages = {235--238},
       title = {{Simple Interpretations among Complicated Theories}},
       volume = {35},
       year = {1990},
  }
  

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

  @article{Gr90e,
       author = {Erich Gr{\"a}del},
       journal = {SIAM Journal on Computing},
       pages = {787--804},
       title = {{Domino Games and Complexity}},
       volume = {19},
       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 = {Erich Gr{\"a}del},
       journal = {Annals of Pure and Applied Logic},
       pages = {1--30},
       title = {{Dominoes and the Complexity of Subclasses of Logical Theories}},
       volume = {43},
       year = {1989},
  }
  

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

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

• 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,
       address = {Kaiserslautern},
       author = {Erich Gr{\"a}del},
       booktitle = {{Proceedings of 3rd Workshop on Computer Science Logic CSL `89}},
       title = {{On logical descriptions of some concepts in structural complexity theory}},
       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,
       address = {Mantova},
       author = {Erich Gr{\"a}del},
       booktitle = {{Proceedings of 3rd Italian Conference on Theoretical Computer Science}},
       note = {See also: journal version \cite{Gr90b}},
       pages = {323--334},
       publisher = {World Scientific Publishing Co.},
       title = {{On the Notion of Linear Time Computability}},
       year = {1989},
  }
  

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 = {Erich Gr{\"a}del},
       journal = {Theoretical Computer Science},
       pages = {289--301},
       title = {{Subclasses of Presburger Arithmetic and the Polynomial-Time Hierarchy}},
       volume = {56},
       year = {1988},
  }
  

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

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

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

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

1987

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

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