2012/12/28 by Manfred Kufleitner, Kufleitner, Manfred, Alexander Lauser +1
Computer Science · #Advanced Algebra and Logic #F.4.1 #F.4.3 #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #cs.FL #cs.LO #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.1212.6500
Accepted at STACS 2013
arxiv created 2012/12/28 · openalex publication_date 2012/12/28 · arxiv updated 2013/01/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We consider the quantifier alternation hierarchy within two-variable first-order logic FO2[<,suc] over finite words with linear order and binary successor predicate. We give a single identity of omega-terms for each level of this hierarchy. This shows that it is decidable for a given regular language and a non-negative integer m, whether the language is definable by a formula in FO2[<,suc] which has at most m quantifier alternations. We also consider the alternation hierarchy of unary temporal logic TL[X,F,Y,P] defined by the maximal number of nested negations. This hierarchy coincides with the FO2[<,suc] alternation hierarchy.