2026-07-23T17:27:45Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:19007 2024-03-06T11:03:15Z ddc:004 open_access

Universal Quantification Makes Automatic Structures Hard to Decide Haase, Christoph Piórkowski, Radosław automatic structures universal projection state complexity tiling problems 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Christoph Haase and Radosław Piórkowski 2023 Is Part Of LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2023.13 urn:nbn:de:0030-drops-190075 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.13 eng https://creativecommons.org/licenses/by/4.0/legalcode