Kallas, Jakub ;
Kufleitner, Manfred ;
Lauser, Alexander
Firstorder Fragments with Successor over Infinite Words
Abstract
We consider fragments of firstorder 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 FO^2 = 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 $L$ is in FO^2 cap Sigma_2 if and only if $L$ is the interior of an FO^2 language. Symmetrically, a language is in FO^2 cap Pi_2 if and only if it is the topological closure of an FO^2 language. The fragment Delta_2 = Sigma_2 cap Pi_2 contains exactly the clopen languages in FO^2. In particular, over infinite words Delta_2 is a strict subclass of 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 dotdepth 3/2 over finite words.
Decidability of dotdepth 3/2 over finite words was first shown by Glasser and Schmitz in STACS 2000, and decidability of the membership problem for FO^2 over infinite words was shown 1998 by Wilke in his habilitation thesis whereas decidability of Sigma_2 over infinite words is new.
BibTeX  Entry
@InProceedings{kallas_et_al:LIPIcs:2011:3026,
author = {Jakub Kallas and Manfred Kufleitner and Alexander Lauser},
title = {{Firstorder Fragments with Successor over Infinite Words}},
booktitle = {28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011) },
pages = {356367},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783939897255},
ISSN = {18688969},
year = {2011},
volume = {9},
editor = {Thomas Schwentick and Christoph D{\"u}rr},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2011/3026},
URN = {urn:nbn:de:0030drops30267},
doi = {http://dx.doi.org/10.4230/LIPIcs.STACS.2011.356},
annote = {Keywords: infinite words, regular languages, firstorder logic, automata theory, semigroups, topology}
}
Keywords: 

infinite words, regular languages, firstorder logic, automata theory, semigroups, topology 
Seminar: 

28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011)

Issue date: 

2011 
Date of publication: 

2011 