License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2023.13
URN: urn:nbn:de:0030-drops-190075
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/19007/
Go to the corresponding LIPIcs Volume Portal

Haase, Christoph ; Piórkowski, Radosław

Universal Quantification Makes Automatic Structures Hard to Decide

pdf-format:
LIPIcs-CONCUR-2023-13.pdf (1 MB)

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.

BibTeX - Entry

@InProceedings{haase_et_al:LIPIcs.CONCUR.2023.13,
  author =	{Haase, Christoph and Pi\'{o}rkowski, Rados{\l}aw},
  title =	{{Universal Quantification Makes Automatic Structures Hard to Decide}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{13:1--13:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2023/19007},
  URN =		{urn:nbn:de:0030-drops-190075},
  doi =		{10.4230/LIPIcs.CONCUR.2023.13},
  annote =	{Keywords: automatic structures, universal projection, state complexity, tiling problems}
}

Keywords: automatic structures, universal projection, state complexity, tiling problems
Collection: 34th International Conference on Concurrency Theory (CONCUR 2023)
Issue Date: 2023
Date of publication: 07.09.2023

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI