License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2012.426
URN: urn:nbn:de:0030-drops-36888
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2012/3688/
Go to the corresponding LIPIcs Volume Portal

Kufleitner, Manfred ; Weil, Pascal

The FO2 alternation hierarchy is decidable

pdf-format:
34.pdf (0.6 MB)

Abstract

We consider the two-variable fragment FO2[<] of first-order
logic over finite words. Numerous characterizations of this class are
known. Therien and Wilke have shown that it is decidable whether a
given regular language is definable in FO2[<]. From a practical
point of view, as shown by Weis, FO2[<] is interesting since its
satisfiability problem is in NP. Restricting the number of
quantifier alternations yields an infinite hierarchy inside the class
of FO2[<]-definable languages. We show that each level of this
hierarchy is decidable. For this purpose, we relate each level of the
hierarchy with a decidable variety of finite monoids.

Our result implies that there are many different ways of climbing up
the FO2[<]-quantifier alternation hierarchy: deterministic and
co-deterministic products, Mal'cev products with definite and reverse
definite semigroups, iterated block products with J-trivial
monoids, and some inductively defined omega-term identities. A
combinatorial tool in the process of ascension is that of condensed
rankers, a refinement of the rankers of Weis and Immerman and the
turtle programs of Schwentick, Therien, and Vollmer.

BibTeX - Entry

@InProceedings{kufleitner_et_al:LIPIcs:2012:3688,
  author =	{Manfred Kufleitner and Pascal Weil},
  title =	{{The FO2 alternation hierarchy is decidable}},
  booktitle =	{Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
  pages =	{426--439},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-42-2},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{16},
  editor =	{Patrick C{\'e}gielski and Arnaud Durand},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2012/3688},
  URN =		{urn:nbn:de:0030-drops-36888},
  doi =		{10.4230/LIPIcs.CSL.2012.426},
  annote =	{Keywords: first-order logic, regular language, automata theory, semigroup, ranker}
}

Keywords: first-order logic, regular language, automata theory, semigroup, ranker
Collection: Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL
Issue Date: 2012
Date of publication: 03.09.2012

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