Weis, Philipp ;
Immerman, Neil
Structure Theorem and Strict Alternation Hierarchy for FOÃ‚Â² on Words
Abstract
It is wellknown that every firstorder property on words is
expressible using at most three variables. The subclass of properties
expressible with only two variables is also quite interesting and
wellstudied. We prove precise structure
theorems that characterize the exact expressive power of firstorder
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 = {18624405},
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, EhrenfeuchtFraisse games}
}
Keywords: 

Descriptive complexity, finite model theory, alternation hierarchy, EhrenfeuchtFraisse games 
Seminar: 

06451  Circuits, Logic, and Games

Issue date: 

2007 
Date of publication: 

23.04.2007 