2026-07-22T06:25:55Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:4949 2024-03-06T10:35:37Z ddc:004 open_access

Separation and the Successor Relation Place, Thomas Zeitoun, Marc separation problem regular word languages logics decidable characterizations semidirect product We investigate two problems for a class C of regular word languages. The C-membership problem asks for an algorithm to decide whether an input language belongs to C. The C-separation problem asks for an algorithm that, given as input two regular languages, decides whether there exists a third language in C containing the first language, while being disjoint from the second. These problems are considered as means to obtain a deep understanding of the class C. It is usual for such classes to be defined by logical formalisms. Logics are often built on top of each other, by adding new predicates. A natural construction is to enrich a logic with the successor relation. In this paper, we obtain new and simple proofs of two transfer results: we show that for suitable logically defined classes, the membership, resp. the separation problem for a class enriched with the successor relation reduces to the same problem for the original class. Our reductions work both for languages of finite words and infinite words. The proofs are mostly self-contained, and only require a basic background on regular languages. This paper therefore gives simple proofs of results that were considered as difficult, such as the decidability of the membership problem for the levels 1, 3/2, 2 and 5/2 of the dot-depth hierarchy. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Thomas Place and Marc Zeitoun 2015 Is Part Of LIPIcs, Volume 30, 32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.STACS.2015.662 urn:nbn:de:0030-drops-49499 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2015.662 eng https://creativecommons.org/licenses/by/3.0/legalcode