@TechReport{ KufleitnerL13tr,
author = "Manfred Kufleitner and Alexander Lauser",
title = "Nesting Negations in $\mathrm{FO}^{2}$ over Finite Words",
institution = "University of Stuttgart",
pages = "19",
type = "Technical Report Computer Science",
number = "2013/07",
month = "9",
year = "2013",
keywords = "regular language; finite monoid; positive variety;
first-order logic",
language = "English",
address = "University of Stuttgart, Institute of Formal Methods in
Computer Science, Theoretical Computer Science",
abstract = "We consider the fragment $\Sigma^{2}_{m}$ of two-variable
first-order logic $\mathrm{FO}^{2}[<]$ over finite words
which is defined by restricting the nesting depth of
negations to at most m. Our first result is a combinatorial
characterization of $\Sigma^{2}_{m}$ in terms of so-called
rankers. This generalizes a result by Weis and Immerman
which we recover as an immediate consequence.
Our second result is an effective algebraic
characterization of $\Sigma^{2}_{m}$, i.e., for every
integer m one can decide whether a given regular language
is definable by a two-variable first-order formula with
negation nesting depth at most m. More precisely, for every
$m$ we give omega-terms $U_{m}$ and $V_{m}$ such that an
$\mathrm{FO}^{2}$-definable language is in $\Sigma^{2}_{m}$
if and only if its ordered syntactic monoid satisfies the
identity $U_{m} \le V_{m}$."
}