LIPIcs.CONCUR.2023.13.pdf
- Filesize: 1.05 MB
- 17 pages
Document
Universal Quantification Makes Automatic Structures Hard to Decide
Authors
Christoph Haase 
,
Radosław Piórkowski
-
Part of:
Volume:
34th International Conference on Concurrency Theory (CONCUR 2023)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Concurrency Theory (CONCUR) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2023-09-07
File
Document Identifiers
Author Details
Acknowledgements
We would like to thank the anonymous reviewers for their comments and suggestions, which helped us to improve the presentation of this paper. We are grateful to Alessio Mansutti for spotting a bug in Section 4.
Cite AsGet BibTex
Christoph Haase and Radosław Piórkowski. Universal Quantification Makes Automatic Structures Hard to Decide. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 13:1-13:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CONCUR.2023.13
https://doi.org/10.4230/LIPIcs.CONCUR.2023.13
Abstract
Automatic structures are structures whose universe and relations can be represented as regular languages. It follows from the standard closure properties of regular languages that the first-order theory of an automatic structure is decidable. While existential quantifiers can be eliminated in linear time by application of a homomorphism, universal quantifiers are commonly eliminated via the identity ∀x.Φ≡¬(∃x.¬Φ). If Φ is represented in the standard way as an NFA, a priori this approach results in a doubly exponential blow-up. However, the recent literature has shown that there are classes of automatic structures for which universal quantifiers can be eliminated by different means without this blow-up by treating them as first-class citizens and not resorting to double complementation. While existing lower bounds for some classes of automatic structures show that a singly exponential blow-up is unavoidable when eliminating a universal quantifier, it is not known whether there may be better approaches that avoid the naïve doubly exponential blow-up, perhaps at least in restricted settings.
In this paper, we answer this question negatively and show that there is a family of NFA representing automatic relations for which the minimal NFA recognising the language after eliminating a single universal quantifier is doubly exponential, and deciding whether this language is empty is ExpSpace-complete.
Subject Classification
ACM Subject Classification
- Theory of computation → Logic
Keywords
- automatic structures
- universal projection
- state complexity
- tiling problems
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- The LASH toolset. URL: https://people.montefiore.uliege.be/boigelot/research/lash/index.html.
- Achim Blumensath and Erich Grädel. Automatic structures. In Logic in Computer Science, LICS, pages 51-62. IEEE Computer Society, 2000. URL: https://doi.org/10.1109/LICS.2000.855755.
- Bernard Boigelot, Pascal Fontaine, and Baptiste Vergain. First-order quantification over automata. In Conference on Implementation and Application of Automata, CIAA, Lect. Notes Comp. Sci. Springer, 2023. To appear. URL: https://doi.org/10.48550/arXiv.2306.04210.
-
Véronique Bruyère. Entiers et automates finis. Mémoire de fin d’études, 1985.
- Véronique Bruyère, Georges Hansel, Christian Michaux, and Roger Villemaire. Logic and p-recognizable sets of integers. Bull. Belg. Math. Soc. Simon Stevin, 1(2):191-238, 1994. URL: https://doi.org/10.36045/bbms/1103408547.
- J. Richard Büchi. Weak second-order arithmetic and finite automata. Math. Logic Quart., 6(1‐6):66-92, 1960. URL: https://doi.org/10.1002/malq.19600060105.
- Dmitry Chistikov and Christoph Haase. On the complexity of quantified integer programming. In International Colloquium on Automata, Languages, and Programming, ICALP, volume 80 of LIPIcs, pages 94:1-94:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.ICALP.2017.94.
- Dmitry Chistikov, Christoph Haase, and Alessio Mansutti. Geometric decision procedures and the VC dimension of linear arithmetic theories. In Logic in Computer Science, LICS, pages 59:1-59:13. ACM, 2022. URL: https://doi.org/10.1145/3531130.3533372.
- Antoine Durand-Gasselin and Peter Habermehl. Ehrenfeucht-fraïssé goes elementarily automatic for structures of bounded degree. In Symposium on Theoretical Aspects of Computer Science, STACS, volume 14 of LIPIcs, pages 242-253. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. URL: https://doi.org/10.4230/LIPIcs.STACS.2012.242.
-
Seymour Ginsburg and Edwin H. Spanier. Semigroups, Presburger formulas, and languages. Pac. J. Math., 16(2):285-296, 1966.
- Bernard R. Hodgson. On direct products of automaton decidable theories. Theor. Comput. Sci., 19(3):331-335, 1982. URL: https://doi.org/10.1016/0304-3975(82)90042-1.
- Bakhadyr Khoussainov and Anil Nerode. Automatic presentations of structures. In Logical and Computational Complexity, LCC, volume 960 of Lect. Notes Comp. Sci., pages 367-392. Springer, 1995. URL: https://doi.org/10.1007/3-540-60178-3_93.
- Dietrich Kuske. Theories of automatic structures and their complexity. In Conference on Algebraic Informatics, CAI, volume 5725 of Lect. Notes Comp. Sci., pages 81-98. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-03564-7_5.
- Dietrich Kuske and Markus Lohrey. Automatic structures of bounded degree revisited. J. Symb. Log., 76(4):1352-1380, 2011. URL: https://doi.org/10.2178/jsl/1318338854.
- Jérôme Leroux and Gérald Point. TaPAS: The Talence Presburger Arithmetic Suite. In Tools and Algorithms for the Construction and Analysis of Systems, TACAS, volume 5505 of Lect. Notes Comp. Sci., pages 182-185. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-00768-2_18.
- Hamoon Mousavi. Automatic theorem proving in Walnut. CoRR, 2016. URL: https://arxiv.org/abs/1603.06017.
-
Mojżesz Presburger. Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In Comptes Rendus du I congres de Mathematiciens des Pays Slaves, pages 92-101. 1929.
- François Schwarzentruber. The complexity of tiling problems, 2019. URL: https://arxiv.org/abs/1907.00102.
- Ken Thompson. Programming techniques: Regular expression search algorithm. Commun. ACM, 11(6):419-422, 1968. URL: https://doi.org/10.1145/363347.363387.