Algorithmic Model Theory


Finite model theory studies the relationship between logical definability and computational complexity on finite structures. A particularly important aspect concerns logical descriptions of complexity classes. Our research group has made significant contributions to this area.

A newer development in this field is the extension of the approach and methodology of finite model theory to (particular classes of) infinite structures. Algorithmic issues on infinite structures are of increasing importance in several areas of computer science. In databases, the traditional model based on finite relational structures has turned out to be inadequate for modern applications (like geographic data, constraint databases, data on the Web). Also in verification, infinite (but finitely presentable) transition systems become more and more important, in particular for applications to software.

We investigate several directions, for making the methodology developed in finite model theory applicable to infinite structures. Of particular importance are, again, the connections between algorithmic issues and logical definability.

We have developed a model theory of metafinite structures that combine finite structures with arithmetic operations on infinite numerical domains. Applications of metafinite model theory have been studied in the following domains: descriptive complexity on real numbers, approximation properties of optimization and counting problems, databases with uncertain or unreliable information, and database query languages with aggregates.

We study algorithmic and definability issues on various classes of infinite structures that are presentable by automata and interpretations. The work by A. Blumensath, V. Bárány, and E. Grädel on automatic structures has been very influential for the development of this field.


Open Problems

  • We maintain a collection of Open Problems in Finite Model Theory. (Last updated August 21, 2003.)
  • New problems (at most half a page) and announcements of solutions (at most one page) should be sent to Erich Grädel or Richard Wilke, preferably in LaTeX.



Finite and Algorithmic Model Theory

Workshop on Logic, Language, Information and Computation


Erich Grädel, Richard Wilke