Document Open Access Logo

Complexity of Counting First-Order Logic for the Subword Order

Authors Dietrich Kuske, Christian Schwarz

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2020.61.pdf
  • Filesize: 437 kB
  • 12 pages

Document Identifiers

Author Details

Dietrich Kuske
  • Technische Universität Ilmenau, Germany
Christian Schwarz
  • Technische Universität Ilmenau, Germany

Cite As Get BibTex

Dietrich Kuske and Christian Schwarz. Complexity of Counting First-Order Logic for the Subword Order. In 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 170, pp. 61:1-61:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.MFCS.2020.61

Abstract

This paper considers the structure consisting of the set of all words over a given alphabet together with the subword relation, regular predicates, and constants for every word. We are interested in the counting extension of first-order logic by threshold counting quantifiers. The main result shows that the two-variable fragment of this logic can be decided in two-fold exponential space provided the regular predicates are restricted to piecewise testable ones. This result improves prior insights by Karandikar and Schnoebelen by extending the logic and saving one exponent. Its proof consists of two main parts: First, we provide a quantifier elimination procedure that results in a formula with constants of bounded length (this generalizes the procedure by Karandikar and Schnoebelen for first-order logic). From this, it follows that quantification in formulas can be restricted to words of bounded length, i.e., the second part of the proof is an adaptation of the method by Ferrante and Rackoff to counting logic and deviates significantly from the path of reasoning by Karandikar and Schnoebelen.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Regular languages
Keywords
  • Counting logic
  • piecewise testable languages

Metrics

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

References

  1. J. Ferrante and Ch. Rackoff. The computational complexity of logical theories. Lecture Notes in Mathematics, vol. 718. Springer, 1979. Google Scholar
  2. A. Finkel and Ph. Schnoebelen. Well-structured transition systems everywhere! Theoretical Computer Science, 256:63-92, 2001. Google Scholar
  3. S. Halfon, Ph. Schnoebelen, and G. Zetzsche. Decidability, complexity, and expressiveness of first-order logic over the subword ordering. In LICS'17, pages 1-12. IEEE Computer Society, 2017. Google Scholar
  4. G. Higman. Ordering by divisibility in abstract algebras. Proc. London Math. Soc., 2:326-336, 1952. Google Scholar
  5. J. Ježek and R. McKenzie. Definability in substructure orderings. I: Finite semilattices. Algebra Univers., 61(1):59-75, 2009. Google Scholar
  6. P. Karandikar and Ph. Schnoebelen. Decidability in the logic of subsequences and supersequences. In FSTTCS'15, Leibniz International Proceedings in Informatics (LIPIcs) vol. 45, pages 84-97. Leibniz-Zentrum für Informatik, 2015. Google Scholar
  7. P. Karandikar and Ph. Schnoebelen. The height of piecewise-testable languages and the complexity of the logic of subwords. Logical Methods in Computer Science, 15(2), 2019. Google Scholar
  8. O. V. Kudinov and V. L. Selivanov. Undecidability in the homomorphic quasiorder of finite labelled forests. J. Log. Comput., 17(6):1135-1151, 2007. Google Scholar
  9. O. V. Kudinov, V. L. Selivanov, and L. V. Yartseva. Definability in the subword order. In CiE'10, Lecture Notes in Comp. Science vol. 6158, pages 246-255. Springer, 2010. Google Scholar
  10. O. V. Kudinov, V. L. Selivanov, and A. V. Zhukov. Definability in the h-quasiorder of labeled forests. Ann. Pure Appl. Logic, 159(3):318-332, 2009. Google Scholar
  11. D. Kuske. Theories of orders on the set of words. Theoretical Informatics and Applications, 40:53-74, 2006. Google Scholar
  12. D. Kuske. The subtrace order and counting first-order logic. In CSR'20, Lecture Notes in Comp. Science vol. 12159, pages 289-302. Springer, 2020. Google Scholar
  13. D. Kuske and G. Zetzsche. Languages ordered by the subword order. In FoSSaCS'19, Lecture Notes in Comp. Science vol. 11425, pages 348-364. Springer, 2019. Google Scholar
  14. M. Lothaire. Combinatorics on Words. Addison-Wesley, 1983. Google Scholar
  15. T. Masopust. Piecewise testable languages and nondeterministic automata. In MFCS'16, Leibniz International Proceedings in Informatics (LIPIcs) vol. 58, pages 67:1-67:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. Google Scholar
  16. T. Masopust and M. Thomazo. On boolean combinations forming piecewise testable languages. Theoretical Computer Science, 682:165-179, 2017. Google Scholar
  17. Ph. Schnoebelen. personal communication, February 2020. Google Scholar
  18. I. Simon. Hierarchies of events with dot-depth one. PhD thesis, University of Waterloo, 1972. Google Scholar
  19. I. Simon. Piecewise testable events. In Automata Theory and Formal Languages, Lecture Notes in Comp. Science vol. 33, pages 214-222. Springer, 1975. Google Scholar
  20. Ramanathan S. Thinniyam. Definability of recursive predicates in the induced subgraph order. In 7th Indian Conference on Logic and Its Applications (ICLA'17), Lecture Notes in Comp. Science vol. 10119, pages 211-223. Springer, 2017. Google Scholar
  21. Ramanathan S. Thinniyam. Defining recursive predicates in graph orders. Logical Methods in Computer Science, 14(3), 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 About DROPS Imprint Privacy Contact