Weis, Philipp ;
Immerman, Neil
Structure Theorem and Strict Alternation Hierarchy for FO² on Words
Abstract
It is well-known that every first-order property on words is
expressible using at most three variables. The subclass of properties
expressible with only two variables is also quite interesting and
well-studied. We prove precise structure
theorems that characterize the exact expressive power of first-order
logic with two variables on words. Our results apply to
FO$^2[<]$ and FO$^2[<,suc]$, the latter of which includes the
binary successor relation in addition to the linear ordering on
string positions.
For both languages, our structure theorems show exactly what is
expressible using a given quantifier depth, $n$, and using $m$ blocks
of alternating quantifiers, for any $mleq n$. Using these
characterizations, we prove, among other results, that there is a
strict hierarchy of alternating quantifiers for both languages. The
question whether there was such a hierarchy had been completely open
since it was asked in [Etessami, Vardi, and Wilke 1997].
BibTeX - Entry
@InProceedings{weis_et_al:DSP:2007:975,
author = {Philipp Weis and Neil Immerman},
title = {Structure Theorem and Strict Alternation Hierarchy for FO² on Words},
booktitle = {Circuits, Logic, and Games},
year = {2007},
editor = {Thomas Schwentick and Denis Th{\'e}rien and Heribert Vollmer },
number = {06451},
series = {Dagstuhl Seminar Proceedings},
ISSN = {1862-4405},
publisher = {Internationales Begegnungs- und Forschungszentrum f{\"u}r Informatik (IBFI), Schloss Dagstuhl, Germany},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2007/975},
annote = {Keywords: Descriptive complexity, finite model theory, alternation hierarchy, Ehrenfeucht-Fraisse games}
}
|
Keywords: |
|
Descriptive complexity, finite model theory, alternation hierarchy, Ehrenfeucht-Fraisse games |
|
Seminar: |
|
06451 - Circuits, Logic, and Games
|
|
Documenttype: |
|
InProceedings |
|
Issue date: |
|
2007 |
|
Date of publication: |
|
23.04.2007 |