Adding successor: A transfer theorem for separation and covering

TL;DR

This paper introduces a transfer theorem that reduces the separation and covering problems for enriched logical classes with successor relations to their base classes, simplifying analysis for both finite and infinite words.

Contribution

It provides a novel transfer result that connects separation and covering problems between logical classes with and without successor relations.

Findings

Separation reduces to base class separation when enriched with successor.

The transfer applies to both finite and infinite word languages.

The results simplify the analysis of logical classes in formal language theory.

Abstract

Given a class C of word languages, 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. Separation is usually investigated as a means to obtain a deep understanding of the class C. In the paper, we are mainly interested in classes defined by logical formalisms. Such classes are often built on top of each other: given some logic, one builds a stronger one by adding new predicates to its signature. A natural construction is to enrich a logic with the successor relation. In this paper, we present a transfer result applying to this construction: we show that for suitable logically defined classes, separation for the logic enriched with the successor relation reduces to separation for the original logic. Our theorem also applies to a problem that is stronger than separation: covering. Moreover, we actually present two reductions: one for languages of finite words and the other for languages of infinite words.