License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DagSemProc.06451.6
URN: urn:nbn:de:0030-drops-9751
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2007/975/
Go to the corresponding Portal

Weis, Philipp ; Immerman, Neil

Structure Theorem and Strict Alternation Hierarchy for FO² on Words

pdf-format:
06451.ImmermanNeil.Paper.975.pdf (0.3 MB)

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:DagSemProc.06451.6,
  author =	{Weis, Philipp and Immerman, Neil},
  title =	{{Structure Theorem and Strict Alternation Hierarchy for FO\~{A}‚\^{A}² on Words}},
  booktitle =	{Circuits, Logic, and Games},
  pages =	{1--22},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{6451},
  editor =	{Thomas Schwentick and Denis Th\'{e}rien and Heribert Vollmer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2007/975},
  URN =		{urn:nbn:de:0030-drops-9751},
  doi =		{10.4230/DagSemProc.06451.6},
  annote =	{Keywords: Descriptive complexity, finite model theory, alternation hierarchy, Ehrenfeucht-Fraisse games}
}

Keywords: Descriptive complexity, finite model theory, alternation hierarchy, Ehrenfeucht-Fraisse games
Collection: 06451 - Circuits, Logic, and Games
Issue Date: 2007
Date of publication: 23.04.2007

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI