**Date:**
Wed 25 Feb

**Time:**
15.00

**Place:**
room 214

**Speaker:**
Georg Gottlob (TU Wien)

**Title:**
Existential Second Order Logic Over Strings

**Reference:**
Eugenio Moggi

**Abstract.**
Second-order logic has attracted the interest of logicians,
mathematicians, and computer scientists for a long time, and many
important results have been obtained which link logic and automata
theory. Two of the most well-known results are the famous Buechi
Theorem, which says that monadic second-order logic (MSO) over strings
precisely characterizes the regular languages, and Fagin's Theorem,
which states that the existential prefix class of second-order logic
(ESO) exactly expresses the NP properties over finite structures (in
particular, over strings). Thus, ESO is a much more expressive logic
over strings than MSO. However, little is known about the relationship
between syntactic fragments of ESO and MSO.
We shed light on this issue by investigating regular prefix classes of
(nonmonadic) ESO, i.e., prefix classes of ESO which express only
regular languages. Our main results are briefly summarized as
follows. Denote by ESO(Q) the prefix class Sigma^1_1(Q), where Q is a
first order prefix class.
- The prefix class ESO(E*AA) is regular.
(Note that model checking for this class is NP-complete over graphs.)
- The prefix class ESO(E*AE*) = ESO(Ackermann) is regular.
(Note that model checking for this class is NP-complete over graphs.)
- Any prefix class ESO(Q) not contained in the union of ESO(E*AA)
and ESO(E*AE*) is not regular, i.e., ESO(E*AA) and ESO(E*AE*)
are the maximal regular standard prefix classes.
1.-3. give a complete characterization of the regular prefix
classes of ESO.
- We obtain the following dichotomy theorem:
Let ESO(Q) be any prefix class. Then, either ESO(Q) is regular, or
ESO(Q) expresses some NP-complete language.
This means that model checking for ESO(Q) is either possible by a DFA,
or it is NP-complete.
- We give a precise characterization of those prefix classes of ESO
which are equivalent to MSO over strings.
- Assuming NP <> coNP, we give a precise characterization of those
standard prefix classes of ESO which, over strings, are closed under
complement.

The results are joint work with Th. Eiter (Giessen) and Y. Gurevich
(Michigan).