Salvato in:
| Autori principali: | , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2023
|
| Soggetti: | |
| Accesso online: | https://arxiv.org/abs/2306.10432 |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866912958758518784 |
|---|---|
| author | Haase, Christoph Piórkowski, Radoslaw |
| author_facet | Haase, Christoph Piórkowski, Radoslaw |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2306_10432 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Universal quantification makes automatic structures hard to decide Haase, Christoph Piórkowski, Radoslaw Logic in Computer Science 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. |
| title | Universal quantification makes automatic structures hard to decide |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2306.10432 |