Kufleitner, Manfred ;
Weil, Pascal
The FO2 alternation hierarchy is decidable
Abstract
We consider the twovariable fragment FO2[<] of firstorder
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
codeterministic products, Mal'cev products with definite and reverse
definite semigroups, iterated block products with Jtrivial
monoids, and some inductively defined omegaterm 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 = {426439},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783939897422},
ISSN = {18688969},
year = {2012},
volume = {16},
editor = {Patrick C{\'e}gielski and Arnaud Durand},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2012/3688},
URN = {urn:nbn:de:0030drops36888},
doi = {http://dx.doi.org/10.4230/LIPIcs.CSL.2012.426},
annote = {Keywords: firstorder logic, regular language, automata theory, semigroup, ranker}
}
2012
Keywords: 

firstorder logic, regular language, automata theory, semigroup, ranker 
Seminar: 

Computer Science Logic (CSL'12)  26th International Workshop/21st Annual Conference of the EACSL

Related Scholarly Article: 


Issue date: 

2012 
Date of publication: 

2012 