@InProceedings{	  kkl11stacs,
  author	= "Jakub Kallas and Manfred Kufleitner and Alexander Lauser",
  title		= "First-order Fragments with Successor over Infinite Words",
  booktitle	= "28th International Symposium on Theoretical Aspects of
		  Computer Science (STACS) 2011",
  pages		= "356--367",
  series	= "Leibniz International Proceedings in Informatics (LIPIcs)",
  isbn		= "978-3-939897-25-5",
  issn		= "1868-8969",
  year		= "2011",
  volume	= "9",
  editor	= "{\relax Th}omas Schwentick and {\relax Ch}ristoph
		  D{\"u}rr",
  publisher	= "Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik",
  address	= "Dagstuhl, Germany",
  url		= "http://drops.dagstuhl.de/opus/volltexte/2011/3026",
  doi		= "10.4230/LIPIcs.STACS.2011.356",
  abstract	= "We consider fragments of first-order logic and as models
		  we allow finite and infinite words simultaneously. The only
		  binary relations apart from equality are order comparison <
		  and the successor predicate +1. We give characterizations
		  of the fragments $\Sigma_{2} = \Sigma_{2}[<,+1]$ and
		  $\mathrm{FO}^{2} = \mathrm{FO}^{2}[<,+1]$ in terms of
		  algebraic and topological properties. To this end we
		  introduce the factor topology over infinite words. It turns
		  out that a language $\mathrm{L}$ is in the intersection of
		  $\mathrm{FO}^{2}$ and $\Sigma_{2}$ if and only if
		  $\mathrm{L}$ is the interior of an $\mathrm{FO}^{2}$
		  language. Symmetrically, a language is in the intersection
		  of $\mathrm{FO}^{2}$ and $\Pi_{2} if and only if it is the
		  topological closure of an $\mathrm{FO}^{2}$ language. The
		  fragment $\Delta_{2}, which by definition is the
		  intersection of $\Sigma_{2}$ and $\Pi_{2}$ contains exactly
		  the clopen languages in $\mathrm{FO}^{2}$. In particular,
		  over infinite words $\Delta_{2}$ is a strict subclass of
		  $\mathrm{FO}_{2}$. Our characterizations yield decidability
		  of the membership problem for all these fragments over
		  finite and infinite words; and as a corollary we also
		  obtain decidability for infinite words. Moreover, we give a
		  new decidable algebraic characterization of dot-depth 3/2
		  over finite words.
		  
		  Decidability of dot-depth 3/2 over finite words was first
		  shown by Gla{\ss}er and Schmitz in STACS 2000, and
		  decidability of the membership problem for
		  $\mathrm{FO}_{2}$ over infinite words was shown 1998 by
		  Wilke in his habilitation thesis whereas decidability of
		  $\Sigma_{2}$ over infinite words was not known before."
}