03. – 08. Oktober 1999, Dagstuhl-Seminar 99401

Finite Model Theory, Databases, and Computer-Aided Verification


G. Gottlob (Vienna), E. Grädel (Aachen), M. Vardi (Houston), V. Vianu (San Diego)

Auskunft zu diesem Dagstuhl-Seminar erteilt

Dagstuhl Service Team


Dagstuhl-Seminar-Report 253

The goal of this seminar is to bring together researchers working in finite model theory (FMT), in databases (DB) and in computer-aided verification (CAV). Besides complexity theory, DB and CAV are the two main application areas of FMT in computer science.

A common concern of FMT, DB and CAV is the design and study of logical formalisms with the 'right' balance between expressiveness and complexity. In databases, query languages are developed that should be expressive enough for the relevant queries of a given application area, but nevertheless lend themselves to efficient strategies for query evaluation. In CAV, specification languages are sought that are able to express relevant fairness and liveness conditions, but can be efficiently checked on the important classes of transition systems. In FMT, one studies the relationship between logical definability and computational complexity systematically. One of the central open problem of FMT is the quest for logics that precisely capture the most important complexity classes, in particular the problem whether there is a logic for Ptime. Hence model checking problems, in the broad sense of finding algorithms for and studying the complexity of the evaluation of logical formulae (queries, specifications) in a structure (database, transition system), play a central role in all three fields.

Also the central logical formalisms in the three fields are of a very similar nature. Typically, a basic formalism like first-order logic, relational calculus or modal logic is extended by recursion in one form or another. In particular, fixed-point logics (formalisms that include least and/or greatest fixed points as their essential feature) play a central role in all three fields. In databases, fixed-point and while queries have been studied quite intensively and fixed-point query languages such Datalog and its extensions are central to the field. In CAV, the d -calculus is in some sense the quintessential specification language, since it subsumes most of the other common formalisms like PDL, CTL, CTL* etc. The discovery of natural symbolic evaluation of the d -calculus has lead to the industrial acceptance of computer-aided verification. In FMT, the most important logics are the fixed-point logics LFP, IFP, PFP with a very close relationship to the most important complexity classes. Hence fixed point logics, their expressive power and the algorithmic problems connected with them will be a central topic of this seminar.

Beyond finite structures:

In all three communities the main focus has for many years been on finite structures (databases, transition systems). Interestingly all three communities have recently started to extend their methods to suitable classes of infinite structures. New applications like spatial (geographical) databases have lead to the study of infinite database models, notably constraint databases. In CAV, model checking problems on infinite transition systems such as context-free systems or push-down system have been successfully studied and are of increasing interest also for practical applications. Also the general approach and the techniques of FMT have been extended to suitable classes of infinite structures (e.g. metafinite structures or recursive structures), which seems to be one of the most promising perspectives of finite model theory for the future. In fact this new perspective has been partially motivated by the new developments in databases and CAV.

We expect that the seminar will help to increase the awareness of the researchers working in one field of the problems and methods in the others and thus to increase the interaction and collaboration of the three fields, and the transfer of methodologies from one field to another.


In der Reihe Dagstuhl Reports werden alle Dagstuhl-Seminare und Dagstuhl-Perspektiven-Workshops dokumentiert. Die Organisatoren stellen zusammen mit dem Collector des Seminars einen Bericht zusammen, der die Beiträge der Autoren zusammenfasst und um eine Zusammenfassung ergänzt.


Download Übersichtsflyer (PDF).


Es besteht weiterhin die Möglichkeit, eine umfassende Kollektion begutachteter Arbeiten in der Reihe Dagstuhl Follow-Ups zu publizieren.

Dagstuhl's Impact

Bitte informieren Sie uns, wenn eine Veröffentlichung ausgehend von
Ihrem Seminar entsteht. Derartige Veröffentlichungen werden von uns in der Rubrik Dagstuhl's Impact separat aufgelistet  und im Erdgeschoss der Bibliothek präsentiert.