A Transfer Theorem for the Separation Problem

TL;DR

This paper presents transfer theorems that reduce the membership and separation problems for enriched classes of regular languages with successor relations to the original classes, simplifying the analysis of logical language classes.

Contribution

It provides simple, self-contained proofs of transfer results for classes enriched with successor, applicable to finite and infinite words, aiding understanding of logical language hierarchies.

Findings

Reduces separation problem to original class for enriched classes

Applies to both finite and infinite words

Simplifies proofs of decidability for levels of the dot-depth hierarchy

Abstract

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 simple self-contained 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 new, simple proofs of results that were considered as difficult, such as the decid- ability of the membership problem for the levels 1, 3/2, 2 and 5/2 of the dot-depth hierarchy.