Seminar Logic, Complexity, Games: Automatic Structures

WS 2020/21

News

Registration

Students with a subject in mathematics can apply by writing an email to seminar [AT] logic.rwth-aachen.de including their name, immatriculation no., subject of studies, no. of semesters of studies, and information about relevant modules they have passed (especially lectures from our group).

Please further indicate whether you are comfortable with a live kickoff meeting. This would, of course, be in compliance with all hygiene regulations.

Content

Automatic structures are first-order structures, whose elements are identified with the words of a regular language, and whose functions and relations are representable by synchronous finite automata. Finite structures, for instance, are trivially automatic, but the really interesting examples of automatic structures are infinite ones, such as Presburger arithmetic and the infinite binary tree with prefix order and equal length predicate.

Automatic structures are interesting because they provide a natural family of infinite structures that are finitely presentable (by the automata that describe their functions and relations) in such a way that important computational problems, such as first-order model checking or query evaluation, can be handled effectively. Automatic structures thus provide a domain of structures that is relevant for the programme of computational model theory, i.e. the study of logical definability and computational complexity of finitely presentable structures. Computational model theory builds on, and extends finite model theory; it translates computational problems to logical ones and tackles them using tools of logic. This approach has been quite successful for finite structures where we have numerous characterisation theorems relating machine models and computational complexity classes with various logics and definability within these logics. The traditional limitation to finite structures is, however, unnecessarily restrictive, as there are many applications, e.g., in the fields of databases or automated verification, which naturally call for infinite models. This motivates the extension of methods of finite model theory to relevant domains of infinite structures. Of course, infinite objects handled by computers must be finitely representable in some way, and given a finite representation of a structure, the relevant computational problems concerning the structure should be effectively solvable. Automatic structures provide one such framework based on a robust and sufficiently simple, and very well-studied model of computation.

Automatic structures are also relevant in certain branches of mathematics, such as computational group theory. Indeed, the best studied examples of automatic structures are automatic groups, i.e. finitely generated groups with an automatic Cayley graph. The importance of this notion in computational group theory comes from the fact that an automatic presentation of a group yields (efficient) algorithmic solutions for computational problems (e.g. the word problem) that are undecidable in the general case. There are further interesting connections to the theories of automatic sequences and decidable subsystems of arithmetic. The notion of an automatic structure can be modified and generalised in many directions. By using automata over infinite words, we obtain the notion of omega-automatic structures which, contrary to automatic structures, may have uncountable cardinality. Examples of omega-automatic structures include the additive group of the real numbers, and the tree of finite and infinite binary sequences. Similarly one can use tree-automata to define term-automatic structures.

Literature

[BGR10] 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.
[Bar06] V. Bárány. Invariants of Automatic Presentations and Semi-Synchronous Transductions. In Proceedings of the 23rd Annual Symposium on Theoretical Aspects of Computer Science, STACS 2006 (B. Durand and W. Thomas, Eds.), vol. 3884 of LNCS, pp. 289–300. Springer, 2006.
[Bar07] V. Bárány. Automatic Presentations of Infinite Structures. PhD thesis, RWTH Aachen, 2007.
[Bl99] A. Blumensath. Automatic Structures. Diploma thesis, RWTH-Aachen, 1999.
[BlGr04] A. Blumensath and E. Grädel. Finite presentations of infinite structures: Automata and interpretations. Theory of Computing Systems, vol. 37(6), pp. 641–674, 2004.
[CoLo07] T. Colcombet and C. Löding. Transforming structures by set interpretations. Logical Methods in Computer Science, vol. 3(2), 2007.
[Ep92] D. Epstein, J. Cannon, D. Holt, S. Levy, M. Paterson, and W. Thurston. Word processing in groups. , 1992.
[Fa92] B. Farb. Automatic groups: a guided tour. Enseign. Math.(2), vol. 38(3-4), pp. 291–313, 1992.
[Graedel20] 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.
[HjKhMoNi08] G. Hjorth, B. Khoussainov, A. Montalbán, and A. Nies. From automatic structures to Borel structures. In Logic in Computer Science, 2008. LICS'08. 23rd Annual IEEE Symposium on, pp. 431–441, 2008.
[Hod93] W. Hodges. Model theory. Cambridge University Press, 1993.
[Kai08] Ł. Kaiser. Logic and Games on Automatic Structures. PhD thesis, RWTH Aachen, 2008.
[KhMi07] B. Khoussainov and M. Minnes. Three lectures on automatic structures. In Proceedings of Logic Colloquium, pp. 132–176, 2007.
[KhRuSt03] B. Khoussainov, S. Rubin, and F. Stephan. On Automatic Partial Orders. In LICS, pp. 168–177. IEEE Computer Society, 2003.
[Ku03] D. Kuske. Is Cantor's Theorem Automatic? In Logic for Programming, Artificial Intelligence, and Reasoning, pp. 332–345, 2003.
[KuLiLo10] D. Kuske, J. Liu, and M. Lohrey. The isomorphism problem on classes of automatic structures. In Logic in Computer Science (LICS), 2010 25th Annual IEEE Symposium on, pp. 160–169, 2010.
[KuLo09] D. Kuske and M. Lohrey. Automatic structures of bounded degree revisited. In Computer Science Logic, pp. 364–378, 2009.
[KuNiRuSt07] B. Khoussainov, A. Nies, S. Rubin, and F. Stephan. Automatic Structures: Richness and Limitations. Logical Methods in Computer Science, vol. 3(2), 2007.
[OlTh05] G. P. Oliver and R. M. Thomas. Automatic Presentations for Finitely Generated Groups. In STACS (V. Diekert and B. Durand, Eds.), vol. 3404 of Lecture Notes in Computer Science, pp. 693–704. Springer, 2005.
[Ts11] T. Tsankov. The additive group of the rationals does not have an automatic presentation. Journal for Symbolic Logic (to appear).

Classification

  • Informatik (B.Sc.)/Seminar Informatik
  • Mathematik (B.Sc.)/Seminar: Logik, Komplexität, Spiele
  • Informatik (M.Sc.)/Seminar Theoretische Informatik
  • Mathematik (M.Sc.)/Seminar: Logik, Komplexität, Spiele (Reine Mathematik)
  • Informatik (D)/Hauptstudium/Theoretische Informatik
  • Mathematik (D)/Hauptstudium/Reine Mathematik
  • Informatik (S II)
  • Mathematik (S II)/Hauptstudium/Modul Algebra
  • Mathematik (S II)/Hauptstudium/Modul Angewandte Mathematik

Prerequisites

  • Module Mathematical Logic
  • for B.Sc. Computer Science: Module "Einführung in das wissenschaftliche Arbeiten (Proseminar)"

Contact

Erich Grädel, Katrin Dannert, Matthias Naaf, Benedikt Pago, Richard Wilke