Document Open Access Logo

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

Authors Thomas Place, Marc Zeitoun

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2022.43.pdf
  • Filesize: 0.9 MB
  • 22 pages

Document Identifiers

Author Details

Thomas Place
  • LaBRI, Bordeaux University, France
Marc Zeitoun
  • LaBRI, Bordeaux University, France

Funding

Supported by the DeLTA project (ANR-16-CE40-0007).

Cite AsGet BibTex

Thomas Place and Marc Zeitoun. A Generic Polynomial Time Approach to Separation by First-Order Logic Without Quantifier Alternation. In 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 250, pp. 43:1-43:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.FSTTCS.2022.43

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
  • Theory of computation → Regular languages
Keywords
  • Automata
  • Separation
  • Covering
  • Concatenation hierarchies
  • Group languages

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Jorge Almeida and Marc Zeitoun. The pseudovariety J is hyperdecidable. RAIRO Theoretical Informatics and Applications, 31(5):457-482, 1997. Google Scholar
  2. Mustapha Arfi. Polynomial operations on rational languages. In Proceedings of the 4th Annual Symposium on Theoretical Aspects of Computer Science, STACS'87, pages 198-206, Berlin, Heidelberg, 1987. Springer-Verlag. Google Scholar
  3. Janusz A. Brzozowski and Rina S. Cohen. Dot-depth of star-free events. Journal of Computer and System Sciences, 5(1):1-16, 1971. Google Scholar
  4. Antonio Cano, Giovanna Guaiana, and Jean-Eric Pin. Regular languages and partial commutations. Journal of Information and Computation, 230:76-96, 2013. Google Scholar
  5. Laura Chaubard, Jean Éric Pin, and Howard Straubing. First order formulas with modular predicates. In Proceedings of the 21th IEEE Symposium on Logic in Computer Science (LICS'06), pages 211-220, 2006. Google Scholar
  6. Wojciech Czerwiński, Wim Martens, and Tomáš Masopust. Efficient separability of regular languages by subsequences and suffixes. In Proceedings of the 40th International Colloquium on Automata, Languages, and Programming, ICALP'13, pages 150-161, Berlin, Heidelberg, 2013. Springer-Verlag. Google Scholar
  7. Samuel Eilenberg. Automata, Languages, and Machines, volume B. Academic Press, Inc., Orlando, FL, USA, 1976. Google Scholar
  8. Karsten Henckell, Stuart Margolis, Jean-Eric Pin, and John Rhodes. Ash’s type II theorem, profinite topology and Malcev products. International Journal of Algebra and Computation, 1:411-436, 1991. Google Scholar
  9. Robert Knast. A semigroup characterization of dot-depth one languages. RAIRO - Theoretical Informatics and Applications, 17(4):321-330, 1983. Google Scholar
  10. Alexis Maciel, Pierre Péladeau, and Denis Thérien. Programs over semigroups of dot-depth one. Theoretical Computer Science, 245(1):135-148, 2000. Google Scholar
  11. Stuart Margolis and Jean-Eric Pin. Product of Group Languages. In FCT'85, volume 199 of Lect. Notes Comp. Sci., pages 285-299. Springer-Verlag, 1985. Google Scholar
  12. Tomás Masopust. Separability by piecewise testable languages is ptime-complete. Theor. Comput. Sci., 711:109-114, 2018. Google Scholar
  13. Jean-Eric Pin. Algebraic tools for the concatenation product. Theoretical Computer Science, 292:317-342, 2003. Google Scholar
  14. Jean-Eric Pin. An explicit formula for the intersection of two polynomials of regular languages. In DLT 2013, volume 7907 of Lect. Notes Comp. Sci., pages 31-45. Springer, 2013. Google Scholar
  15. Jean-Eric Pin and Howard Straubing. Some results on 𝒞-varieties. RAIRO - Theoretical Informatics and Applications, 39(1):239-262, 2005. Google Scholar
  16. Thomas Place, Varun Ramanathan, and Pascal Weil. Covering and separation for logical fragments with modular predicates. Logical Methods in Computer Science, 15(2), 2019. Google Scholar
  17. Thomas Place, Lorijn van Rooijen, and Marc Zeitoun. Separating regular languages by piecewise testable and unambiguous languages. In Proceedings of the 38th International Symposium on Mathematical Foundations of Computer Science, MFCS'13, pages 729-740, Berlin, Heidelberg, 2013. Springer-Verlag. Google Scholar
  18. Thomas Place and Marc Zeitoun. Separation for dot-depth two. In Proceedings of the 32th Annual ACM/IEEE Symposium on Logic in Computer Science, (LICS'17), pages 202-213. IEEE Computer Society, 2017. Google Scholar
  19. Thomas Place and Marc Zeitoun. The covering problem. Logical Methods in Computer Science, 14(3), 2018. Google Scholar
  20. Thomas Place and Marc Zeitoun. Generic results for concatenation hierarchies. Theory of Computing Systems (ToCS), 63(4):849-901, 2019. Selected papers from CSR'17. Google Scholar
  21. Thomas Place and Marc Zeitoun. Separation and covering for group based concatenation hierarchies. In Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'19, pages 1-13, 2019. Google Scholar
  22. Thomas Place and Marc Zeitoun. Adding successor: A transfer theorem for separation and covering. ACM Transactions on Computational Logic, 21(2):9:1-9:45, 2020. Google Scholar
  23. Thomas Place and Marc Zeitoun. Separation for dot-depth two. Logical Methods in Computer Science, Volume 17, Issue 3, 2021. Google Scholar
  24. Thomas Place and Marc Zeitoun. Characterizing level one in group-based concatenation hierarchies. In Computer Science - Theory and Applications, Cham, 2022. Springer International Publishing. Google Scholar
  25. Thomas Place and Marc Zeitoun. A generic polynomial time approach to separation by first-order logic without quantifier alternation, 2022. URL: https://doi.org/10.48550/arXiv.2210.00946.
  26. Thomas Place and Marc Zeitoun. Group separation strikes back. To appear, a preliminary version is vailable at https://www.labri.fr/perso/tplace/Files/groups.pdf, 2022.
  27. Imre Simon. Piecewise testable events. In Proceedings of the 2nd GI Conference on Automata Theory and Formal Languages, pages 214-222, Berlin, Heidelberg, 1975. Springer-Verlag. Google Scholar
  28. Benjamin Steinberg. Inevitable graphs and profinite topologies: Some solutions to algorithmic problems in monoid and automata theory, stemming from group theory. International Journal of Algebra and Computation, 11(1):25-72, 2001. Google Scholar
  29. Howard Straubing. A generalization of the schützenberger product of finite monoids. Theoretical Computer Science, 13(2):137-150, 1981. Google Scholar
  30. Howard Straubing. Finite semigroup varieties of the form V asteriskcentered D. Journal of Pure and Applied Algebra, 36:53-94, 1985. Google Scholar
  31. Howard Straubing. On logical descriptions of regular languages. In Proceedings of the 5th Latin American Symposium on Theoretical Informatics, LATIN'02, pages 528-538, Berlin, Heidelberg, 2002. Springer-Verlag. Google Scholar
  32. Denis Thérien. Classification of finite monoids: The language approach. Theoretical Computer Science, 14(2):195-208, 1981. Google Scholar
  33. Gabriel Thierrin. Permutation automata. Theory of Computing Systems, 2(1):83-90, 1968. Google Scholar
  34. Wolfgang Thomas. Classifying regular events in symbolic logic. Journal of Computer and System Sciences, 25(3):360-376, 1982. Google Scholar
  35. Bret Tilson. Categories as algebra: essential ingredient in the theory of monoids. Journal of Pure and Applied Algebra, 48(1):83-198, 1987. Google Scholar
  36. Georg Zetzsche. Separability by piecewise testable languages and downward closures beyond subwords. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'18, pages 929-938, 2018. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact