Algorithmic Model Theory

Introduction: Model Theory and Computation

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 and computations.

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

  • logical definability;
  • 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).

Methodological Issues: Model Theory and Modelling

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 a natural target domain for some modelling task. 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 thetechnical analysis of interesting scenarios, may often consist in striking theright 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 principle limitations (like undecidability or lower bounds on complexities) and primarily technical limitations in terms of the currently available methods.

A A A | Print Print | Impressum Legal note | Contact Contact
    zum Seitenanfangzum Seitenanfang