June 1998: Finite Models and Beyond

Subject: June 1998: Finite Models and Beyond
From: Helmut Veith (kgs-owner@dbai.tuwien.ac.at)
Date: Thu Jun 11 1998 - 15:17:14 MET DST

Finite Models and Beyond

June 17, 18, and 29, 1998

June 17, 1998, 12:00 s.t.

Janos Makowsky, Technion - Israel Institute of Technology
Graphs of bounded clique width and Monadic Second Order Logic

(joint work with B. Courcelle and U. Rotics)

June 18, 1998, 11:00 s.t.

Igor Walukiewicz, Warsaw University
Monadic second order logic, automata and fixpoint calculi

We will present some relationships between the three formalisms
mentioned in the title. We will start with the well known relationships over
words and binary trees. Next we will consider trees of arbitrary degree.
Finally, we will consider tree-like structures. These are structures
obtained by making a countable number of copies of a given structure and
arranging the copies in a tree.

Several results follow from the relationships we are going to present. One
says that MSOL theory of a tree-like structure is decidable if the initially
given structure is decidable. The other gives a characterisation of monadic
second order logic over trees of arbitrary degree in terms of first order
logic with unary fixpoint operators. Yet another one shows that a class of
graphs is definable by a mu-calculus sentence iff it is bisimulation closed
and definable by a sentence of monadic second order logic.

June 18, 1998, 14:00 s.t.

Erich Grädel, RWTH Aachen (currently TU Wien)
Satisfiability and Model Checking for Modal and Non-model Two-variable Logics

Many logics that are of interest for verification, knowlege
representation or other areas of computer science are defined (or can be
viewed) as extensions of modal logics by features like counting constructs,
path quantifiers, transitive closure operators, least and greatest fixed
points etc. Although these additional features are not first-order
constructs, the resulting logics can still be seen as two-variable logics
and are embedded in suitable extensions of FO^2,
first-order logic with two variables.

Therefore decidability and complexity issues for modal and non-modal
two-variable logics have been studied quite intensively in the last years.
It has turned out that satisfiability problems for two-variable logics with
full first-order quantification are usually much harder (and indeed highly
undecidable in many cases) than the satisfiability problems for
corresponding modal logics. On the other side, the situation is different
for model checking problems which have essentially the same complexity for
modal logics as for corresponding two variable logics with full

June 29, 1998, 11:00 s.t.

Marc Spielmann, RWTH Aachen
Choiceless Logspace

We introduce the choiceless fragment of Logspace by means of a
restricted class of Gurevich's abstract state machines, or alternatively, in
terms of an extension of the deterministic transitive closure logic

Choiceless LOGSPACE is more expressive than (FO+DTC) but does not reach full
LOGSPACE on unordered structures. On ordered structures it collapses with

Our work continues the investigation of Blass, Gurevich, and Shelah on the
choiceless fragment of PTIME.

Place: Seminarraum SEM 181A des Instituts für Informationssysteme,
Paniglgasse 16, 1040 Wien, 1. Stock.

Kurt-Gödel-Gesellschaft -- Kurt Gödel Society
Technische Universität Wien, Institut für Computersprachen E185.2,
Resselgasse 3/1, A-1040 Vienna, Austria
Phone: (+43 1) 588 01 ext 4088 email: kgs@logic.tuwien.ac.at Fax: (+43 1) 5041589
WWW: http://logic.tuwien.ac.at/kgs/home.html Listserver: listproc@dbai.tuwien.ac.at
Mit Unterstützung des Bundesministeriums für Wissenschaft und Forschung

This archive was generated by hypermail 2b25 : Thu Apr 06 2000 - 16:19:20 MET DST