Document Open Access Logo

Universal Quantification Makes Automatic Structures Hard to Decide

Authors Christoph Haase , Radosław Piórkowski

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2023.13.pdf
  • Filesize: 1.05 MB
  • 17 pages

Document Identifiers

Author Details

Christoph Haase
  • Department of Computer Science, University of Oxford, UK
Radosław Piórkowski
  • Department of Computer Science, University of Oxford, UK

Funding

This work is part of a project that has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (Grant agreement No. 852769, ARiAT).

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 As Get 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

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)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. The LASH toolset. URL: https://people.montefiore.uliege.be/boigelot/research/lash/index.html.
  2. 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.
  3. 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.
  4. Véronique Bruyère. Entiers et automates finis. Mémoire de fin d’études, 1985. Google Scholar
  5. 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.
  6. 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.
  7. 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.
  8. 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.
  9. 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.
  10. Seymour Ginsburg and Edwin H. Spanier. Semigroups, Presburger formulas, and languages. Pac. J. Math., 16(2):285-296, 1966. Google Scholar
  11. 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.
  12. 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.
  13. 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.
  14. 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.
  15. 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.
  16. Hamoon Mousavi. Automatic theorem proving in Walnut. CoRR, 2016. URL: https://arxiv.org/abs/1603.06017.
  17. 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. Google Scholar
  18. François Schwarzentruber. The complexity of tiling problems, 2019. URL: https://arxiv.org/abs/1907.00102.
  19. Ken Thompson. Programming techniques: Regular expression search algorithm. Commun. ACM, 11(6):419-422, 1968. URL: https://doi.org/10.1145/363347.363387.
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