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: https://drops.dagstuhl.de/opus/volltexte/2022/17435/
Go to the corresponding LIPIcs Volume Portal


Place, Thomas ; Zeitoun, Marc

A Generic Polynomial Time Approach to Separation by First-Order Logic Without Quantifier Alternation

pdf-format:
LIPIcs-FSTTCS-2022-43.pdf (0.9 MB)


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


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI