Universal quantification makes automatic structures hard to decide
Christoph Haase, Radosław Piórkowski
TL;DR
This work proves that emptiness under universal projection for automatic relations is ExpSpace-complete, even for the simplest fixed-variable case $(d=k=1)$, indicating that naïve doubly exponential complementation cannot generally be avoided. It achieves this via a tiling-based reduction that encodes valid computations into automata, and demonstrates that the minimal NFA recognizing the universal projection language can have doubly exponential size. The authors further transfer these lower bounds to fragments of Büchi arithmetic with fixed quantifier prefixes, establishing ExpSpace and 2-ExpSpace hardness results for profiles such as $E^*A^*E^*$ and $E^*A^*E^*A^*$. Complementing the hardness results, an ExpSpace upper bound is provided for the universal-projection emptiness problem, clarifying the precise computational landscape. Overall, the paper shows that universal quantification in automatic structures imposes intrinsic high complexity, with implications for decision procedures and tools handling quantifier elimination over such structures.
Abstract
Automatic structures are first-order 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 $\forall{x}. Φ\equiv \neg (\exists{x}. \neg Φ)$. 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. The techniques underlying our EXPSPACE lower bound further enable us to establish new lower bounds for some fragments of Büchi arithmetic with a fixed number of quantifier alternations.