License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2022.43
URN: urn:nbn:de:0030-drops-174356
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/17435/
Place, Thomas ;
Zeitoun, Marc
A Generic Polynomial Time Approach to Separation by First-Order Logic Without Quantifier Alternation
Abstract
We look at classes of languages associated to fragments of first-order logic BΣ₁, in which quantifier alternations are disallowed. Each such fragment is fully determined by choosing the set of predicates on positions that may be used. Equipping first-order logic with the linear ordering and possibly the successor relation as predicates yields two natural fragments, which were investigated by Simon and Knast, who proved that these two variants have decidable membership: "does an input regular language belong to the class ?". We extend their results in two orthogonal directions.
- First, 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.
- Second, we use more general inputs: classes ? of group languages (i.e., recognized by a DFA in which each letter induces a permutation of the states) and extensions thereof, written ?^+. We rely on a characterization of BΣ₁ by the operator BPol: given an input class ?, it outputs a class BPol(?) that corresponds to a variant of BΣ₁ equipped with special predicates associated to ?. The classes BPol(?) and BPol(?^+) capture many natural variants of BΣ₁ which use predicates such as the linear ordering, the successor, the modular predicates or the alphabetic modular predicates.
We show that separation is decidable for BPol(?) and BPol(?^+) when this is the case for ?. This was already known for BPol(?) and for two particular classes of the form BPol(?^+). Yet, the algorithms were indirect and relied on involved frameworks, yielding poor upper complexity bounds. In contrast, our approach is direct. We work only with elementary concepts (mainly, finite automata). Our main contribution consists in polynomial time Turing reductions from both BPol(?)- and BPol(?^+)-separation to ?-separation. This yields polynomial time algorithms for several key variants of BΣ₁, including those equipped with the linear ordering and possibly the successor and/or the modular predicates.
BibTeX - Entry
@InProceedings{place_et_al:LIPIcs.FSTTCS.2022.43,
author = {Place, Thomas and Zeitoun, Marc},
title = {{A Generic Polynomial Time Approach to Separation by First-Order Logic Without Quantifier Alternation}},
booktitle = {42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)},
pages = {43:1--43:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-261-7},
ISSN = {1868-8969},
year = {2022},
volume = {250},
editor = {Dawar, Anuj and Guruswami, Venkatesan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/17435},
URN = {urn:nbn:de:0030-drops-174356},
doi = {10.4230/LIPIcs.FSTTCS.2022.43},
annote = {Keywords: Automata, Separation, Covering, Concatenation hierarchies, Group languages}
}
|
Keywords: |
|
Automata, Separation, Covering, Concatenation hierarchies, Group languages |
|
Collection: |
|
42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022) |
|
Issue Date: |
|
2022 |
|
Date of publication: |
|
14.12.2022 |
