Intended for researchers and graduate students in theoretical computer science and mathematical logic, this volume contains accessible surveys by leading researchers from areas of current work in logical aspects of computer science, where both finite and infinite model-theoretic methods play an important role. Notably, the articles in this collection emphasize points of contact and connections between finite and infinite model theory in computer science that may suggest new directions for interaction. Among the topics discussed are: algorithmic model theory, descriptive complexity theory, finite model theory, finite variable logic, model checking, model theory for restricted classes of finite structures, and spatial databases. The chapters all include extensive bibliographies facilitating deeper exploration of the literature and further research
Author(s): Esparza J., Michaux C., Steinhorn C. (eds.)
Series: London Mathematical Society Lecture Note Series, Vol. 379
Publisher: CUP
Year: 2011
Language: English
Pages: 355
Contents......Page 6
Preface......Page 8
1.1 Finite presentations of infinite structures......Page 14
1.2 A hierarchy of finitely presentable structures......Page 19
1.2.1 From context-free graphs to prefix-recognisable structures......Page 20
1.2.2 Graph grammars and graph algebras......Page 23
1.2.3 Higher-order data structures......Page 29
1.2.4 Introducing products......Page 32
1.3.1 Fundamentals......Page 39
1.3.2 Examples......Page 41
1.3.3 Injectivity......Page 45
1.3.4 Alternative characterisations......Page 46
1.3.5 Rational graphs......Page 49
1.3.6 Generalisations......Page 50
1.3.7 Subclasses......Page 52
1.3.8 Comparison of classes......Page 54
1.4.1 Beyond first-order logic......Page 55
1.4.2 Complexity of some problems......Page 58
1.4.3 Non-automaticity via pumping and counting......Page 62
1.4.4 Comparing presentations......Page 65
1.4.5 Other notions of automaticity......Page 68
1.5 Automatic Model Theory......Page 75
1.5.1 Model theory restricted to the class of word-automatic structures......Page 76
1.5.2 On the universal word-automatic structure......Page 79
References......Page 82
2.1 Introduction......Page 90
2.3 Capturing first-order geometric properties......Page 91
2.4 First-order topological properties of plain sets......Page 92
2.5 Conclusion on first-order topological properties......Page 101
2.6 Point-based logics for geometric queries......Page 102
2.7 Plane graphs......Page 104
2.8 Spatial datalog and first-order logic extended with a while-loop......Page 105
2.9 First-order logic extended with transitive-closure operators......Page 108
2.10 Expressiveness properties of transitive-closure logics......Page 110
2.11 Deciding termination of transitive-closure logic expressions......Page 113
2.12 Some concluding remarks on transitive-closure logics......Page 119
Bibliography......Page 120
3.1 Introduction......Page 122
3.2.1 Finite variable logic......Page 124
3.2.2 Types......Page 126
3.2.3 Closure maps......Page 127
3.3 Amalgamation classes......Page 128
3.4 Stability......Page 133
3.5 Recursive bounds......Page 137
3.6 Simple, possibly not smoothly approximable structures......Page 139
3.7 Structures on which algebraic closure forms a pregeometry......Page 145
3.8 Questions and problems......Page 149
References......Page 151
4.1 Introduction......Page 153
4.2 Asymptotic classes......Page 155
4.3 Examples of asymptotic classes......Page 157
4.4 Smoothly approximable structures......Page 162
4.5 Asymptotic classes and their ultraproducts......Page 165
4.6 Asymptotic classes of groups......Page 169
4.7 Robust classes......Page 173
4.8 Examples of robust classes......Page 179
4.9 A robust approximation of (Q,<,+)......Page 182
References......Page 187
5.1 Introduction......Page 190
5.2.2 Graphs......Page 193
5.2.3 Logic......Page 195
5.2.4 Complexity......Page 201
5.3 Monadic Second-Order Logic on Tree-Like Structures......Page 206
5.3.1 Tree-Width......Page 207
5.3.2 Tree-Width and Structures......Page 212
5.3.3 Coding Tree-Decompositions in Trees......Page 214
5.3.4 Courcelle's Theorem......Page 221
5.3.5 Seese's Theorem......Page 222
5.4 From Trees to Cliques......Page 223
5.4.1 Clique-Width......Page 224
5.4.2 Rank-Width......Page 229
5.4.3 Monadic Second-Order Logic and Bounded Clique-Width......Page 234
5.4.4 MSO Model-Checking Beyond Tree- and Clique-Width......Page 236
5.5.1 Minors and Minor Ideals......Page 237
5.5.2 Disjoint Paths and the Trinity Lemma......Page 241
5.5.3 The Structure of H-Minor Free Graphs......Page 249
5.5.4 Computing Excluded Minor Characterisations......Page 253
5.6 Monadic Second-Order Logic Revisited......Page 256
5.7.1 Locality of First-Order Logic......Page 258
5.7.2 First-Order Logic on Graphs of Bounded Degree......Page 260
5.7.3 Localisation of Graph Invariants......Page 262
5.7.4 First-Order Logic on H-Minor Free Graphs......Page 265
5.8.1 Classifying Logical Tractability with Respect to Structural Restrictions......Page 270
5.8.2 Limits to Monadic Second-Order Model-Checking......Page 271
5.8.3 Limits to First-Order Model-Checking......Page 274
5.9 Conclusion......Page 277
Acknowledgements......Page 278
References......Page 279
