2026-08-07T14:50:57Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:3026 2024-03-06T10:33:45Z ddc:004 open_access

First-order Fragments with Successor over Infinite Words Kallas, Jakub Kufleitner, Manfred Lauser, Alexander infinite words regular languages first-order logic automata theory semi-groups topology 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 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 dot-depth 3/2 over finite words. Decidability of dot-depth 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Jakub Kallas and Manfred Kufleitner and Alexander Lauser 2011 Is Part Of LIPIcs, Volume 9, 28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.STACS.2011.356 urn:nbn:de:0030-drops-30267 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2011.356 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode