Automatic Structures

We study definability and complexity issues for automatic and ω-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. We explain the notion of (ω-)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 firstorder 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 structur...

• Type: Conference
• Year: 2000
• Where: LICS
• Authors: Achim Blumensath, Erich Grädel
• Keywords: Automated Reasoning, Automatic Structures, Infinite Structures, LICS 2000, ω-automatic Structures