Document

# Complexity of Counting First-Order Logic for the Subword Order

## File

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

## Cite As

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

## References

1. J. Ferrante and Ch. Rackoff. The computational complexity of logical theories. Lecture Notes in Mathematics, vol. 718. Springer, 1979.
2. A. Finkel and Ph. Schnoebelen. Well-structured transition systems everywhere! Theoretical Computer Science, 256:63-92, 2001.
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.
4. G. Higman. Ordering by divisibility in abstract algebras. Proc. London Math. Soc., 2:326-336, 1952.
5. J. Ježek and R. McKenzie. Definability in substructure orderings. I: Finite semilattices. Algebra Univers., 61(1):59-75, 2009.
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.
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.
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.
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.
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.
11. D. Kuske. Theories of orders on the set of words. Theoretical Informatics and Applications, 40:53-74, 2006.
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.
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.
14. M. Lothaire. Combinatorics on Words. Addison-Wesley, 1983.
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.
16. T. Masopust and M. Thomazo. On boolean combinations forming piecewise testable languages. Theoretical Computer Science, 682:165-179, 2017.
17. Ph. Schnoebelen. personal communication, February 2020.
18. I. Simon. Hierarchies of events with dot-depth one. PhD thesis, University of Waterloo, 1972.
19. I. Simon. Piecewise testable events. In Automata Theory and Formal Languages, Lecture Notes in Comp. Science vol. 33, pages 214-222. Springer, 1975.
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.
21. Ramanathan S. Thinniyam. Defining recursive predicates in graph orders. Logical Methods in Computer Science, 14(3), 2018.
X

Feedback for Dagstuhl Publishing