The FO2 alternation hierarchy is decidable

Authors Manfred Kufleitner, Pascal Weil

Thumbnail PDF


  • Filesize: 0.62 MB
  • 14 pages

Document Identifiers

Author Details

Manfred Kufleitner
Pascal Weil

Cite AsGet BibTex

Manfred Kufleitner and Pascal Weil. The FO2 alternation hierarchy is decidable. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 426-439, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)


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.
  • first-order logic
  • regular language
  • automata theory
  • semigroup
  • ranker


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail