Issues in Algorithmic Model Theory for Specific Domains

Martin Otto

(University of Wales Swansea)

Finite model theory provides a framework for the application of model theoretic methods to issues of logic in computer science. As such, it greatly emphasizes the importance of the underlying class of structures to be used in the modelling of application relevant entities. Thinking of typical applications of logic in computer science, however, there is another important issue of the underlying modelling task. This concerns the `grain' or level of abstraction at which the modelling is carried out, or the question up to which notion of equivalence do structures represent the entities which are to be modelled.

A typical example is provided by modal logics and their model theory. The modal domain is characterized not so much by the restriction to special kinds of structures (transition systems, Kripke structures) as by the built-in focus according to which these structures matter only up to bisimulation. At least two other related domains have emerged as important frameworks for the study of algorithmic issues by model theoretic means: the k-variable domains and the guarded domain.

In this talk I shall review old and more recent results in the light of this idea: that the underlying invariance postulates are characteristic of typical domains of applications and call for specific model theoretic tools.
Tuesday 30th November 1999, 15:00
Seminar Room 322
Department of Computer Science