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.

1. The prefix class ESO(E*AA) is regular. (Note that model checking for this class is NP-complete over graphs.)
2. The prefix class ESO(E*AE*) = ESO(Ackermann) is regular. (Note that model checking for this class is NP-complete over graphs.)
3. 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.
4. 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.
5. We give a precise characterization of those prefix classes of ESO which are equivalent to MSO over strings.
6. 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).