| Goal |
| The goal of this workshop was 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. |
| Databases |
| 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. |
| Computer Aided Verification |
|
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. |
| Finite Model Theory |
|
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 P. |
| Model Checking / Logical formalisms |
|
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.
|
|
Fixed-Point Logics
|
|
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 mu-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
mu-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 workshop. |
|
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. |
|
Outcome
|
| The workshop helped to increase the awareness of the researchers
working in one field of the problems and methods in the others and thus
increased the interaction and collaboration of the three fields, and the
transfer of methodologies from one field to another. |
