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

2003

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

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

2002

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

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

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

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

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

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

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

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

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

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

2001

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

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

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

2000

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

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

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

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

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

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

1999

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

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