A generic polynomial time approach to separation by first-order logic without quantifier alternation

TL;DR

This paper develops a polynomial-time method to decide separation problems for certain fragments of first-order logic, extending previous results and providing more efficient algorithms using automata-based techniques.

Contribution

It introduces a direct, automata-based polynomial-time approach for separation in fragments of first-order logic with limited quantifier alternation, generalizing previous indirect methods.

Findings

Decidability of separation for BPol(G) and BPol(G+) classes.

Polynomial-time algorithms for key logical fragments.

Extension to classes with modular and successor predicates.

Abstract

We look at classes of languages associated to the fragment of first-order logic B{\Sigma}1 which disallows quantifier alternations. Each class is defined by choosing the set of predicates on positions that may be used. Two key such fragments are those equipped with the linear ordering and possibly the successor relation. It is known that these two variants have decidable membership: "does an input regular language belong to the class ?". We rely on a characterization of B{\Sigma}1 by the operator BPol: given an input class C, it outputs a class BPol(C) that corresponds to a variant of B{\Sigma}1 equipped with special predicates associated to C. We extend these results in two orthogonal directions. First, we use two kinds of inputs: classes G of group languages (i.e., recognized by a DFA in which each letter induces a permutation of the states) and extensions thereof, written G+. The classes BPol(G) and BPol(G+) capture many variants of B{\Sigma}1 which use predicates such as the linear ordering, the successor, the modular predicates or the alphabetic modular predicates. Second, instead of membership, we explore the more general separation problem: decide if two regular languages can be separated by a language from the class under study. We show it is decidable for BPol(G) and BPol(G+) when this is the case for G. This was known for BPol(G) and for two particular classes BPol(G+). Yet, the algorithms were indirect and relied on involved frameworks, yielding poor upper complexity bounds. Our approach is direct. We work with elementary concepts (mainly, finite automata). Our main contribution consists in polynomial time Turing reductions from both BPol(G)- and BPol(G+)-separation to G-separation. This yields polynomial algorithms for key variants of B{\Sigma}1, including those equipped with the linear ordering and possibly the successor and/or the modular predicates.