Haase, C;
Zetzsche, G;
(2019)
Presburger arithmetic with stars, rational subsets of graph groups, and nested zero tests.
In:
Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS).
IEEE: Vancouver, BC, Canada.
Preview |
Text
Haase_HaaseZetzsche2019a_AAM.pdf - Accepted Version Download (561kB) | Preview |
Abstract
We study the computational complexity of existential Presburger arithmetic with (possibly nested occurrences of) a Kleene-star operator. In addition to being a natural extension of Presburger arithmetic, our investigation is motivated by two other decision problems. The first problem is the rational subset membership problem in graph groups. A graph group is an infinite group specified by a finite undirected graph. While a characterisation of graph groups with a decidable rational subset membership problem was given by Lohrey and Steinberg [J. Algebra, 320(2) (2008)], it has been an open problem (i) whether the decidable fragment has elementary complexity and (ii) what is the complexity for each fixed graph group. The second problem is the reachability problem for integer vector addition systems with states and nested zero tests. We prove that the satisfiability problem for existential Pres-burger arithmetic with stars is NEXP-complete and that all three problems are polynomially inter-reducible. Moreover, we consider for each problem a variant with a fixed parameter: We fix the star-height in the logic, a graph parameter for the membership problem, and the number of distinct zero-tests in the integer vector addition systems. We establish NP-completeness of all problems with fixed parameters. In particular, this enables us to obtain a complete description of the complexity landscape of the rational subset membership problem for fixed graph groups: If the graph is a clique, the problem is N L-complete. If the graph is a disjoint union of cliques, it is P-complete. If it is a transitive forest (and not a union of cliques), the problem is NP-complete. Otherwise, the problem is undecidable.
| Type: | Proceedings paper |
|---|---|
| Title: | Presburger arithmetic with stars, rational subsets of graph groups, and nested zero tests |
| Event: | 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) |
| ISBN-13: | 9781728136080 |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1109/LICS.2019.8785850 |
| Publisher version: | https://doi.org/10.1109/LICS.2019.8785850 |
| Language: | English |
| Additional information: | This version is the author accepted manuscript. For information on re-use, please refer to the publisher’s terms and conditions. |
| Keywords: | Tools, Computational modeling, Computer science, Automata, Grammar, Computational complexity |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/10088915 |
Archive Staff Only
 |
View Item |
