Algorithmic Model Theory

Algorithmic model theory uses tools from mathematical logic to answer model-theoretic questions that arise from algorithmic issues in discrete mathematical structures and in the modelling of data, information and computation.

As a branch of mathematical logic, model theory is generally concerned with the study of

• definability and the expressive power of logical formalisms for the specification of structural properties;
• analysis and classification of the models of given logical specifications.

Immediate algorithmic themes in this context are, for instance,

• decidability and complexity of the logical theories of given structures
  (a classical issue relevant for model checking and verification methodologies);
• connections between the logical and algorithmic complexities of given structural properties.

Model-theoretic questions, which arise from the modelling of computations, specific models of computation or structural representations of data, include

• definability issues over special classes of structures;
• delineation of specialised formalisms designed to capture relevant properties at low levels of complexity;
• delineation of classes of structures with good model-theoretic properties that are rich enough for the modelling of relevant phenomena.

All these issues typically display a sharp trade-off between tractability and richness/expressiveness (of structures/logics).

It is important to note that the basic logical notions of

• logical equivalence (of two specifications),
• satisfiability (of a specification),
• validity (of a deduction)

crucially depend on the underlying class of admissible structures.

Finite model theory, for instance, differs from classical model theory in admitting just finite structures; this restriction is essential for many applications, where infinite instances do not correspond to intended models and hence need to be excluded from all considerations for which the distinction matters. If, for instance, all counter-examples to the equivalence between two specifications or database queries are infinite, then they need to be recognised as equivalent in a setting in which only finite models occur.

Apart from the class of all finite structures, there are many other specific classes of structures that similarly deserve attention – either because they form natural levels with respect to our methods and tools, or because they arise as classes of intended models in some specific context. Similarly, the class of relevant properties may have to be restricted to capture the essence of some modelling scenario: aspects of the structural models that do not correspond to intended aspects of the underlying phenomenon must not make a difference. This imposes specific constraints on the level of granularity at which structural properties are discerned, which in model-theoretic terms typically correspond to preservation properties.

In view of the trade-off mentioned above, the real challenge, besides the technical analysis of interesting scenarios, may often consist in striking a balance between

• the richness of the class of admissible structures
• the expressiveness of the logical formalism or the constraints on structural properties under consideration,

taking into account fundamental limitations (like undecidability or lower bounds on complexities) and primarily technical limitations in terms of the available methods.