UCL Discovery
UCL home » Library Services » Electronic resources » UCL Discovery

Approaching Arithmetic Theories with Finite-State Automata

Haase, C; (2020) Approaching Arithmetic Theories with Finite-State Automata. In: Leporati, A and Martín-Vide, C and Shapira, D and Zandron, C, (eds.) International Conference on Language and Automata Theory and Applications LATA 2020: Language and Automata Theory and Applications. (pp. pp. 33-43). Springer: Milan, Italy. Green open access

[img]
Preview
Text
haa-20.pdf - Accepted version

Download (553kB) | Preview

Abstract

The automata-theoretic approach provides an elegant method for deciding linear arithmetic theories. This approach has recently been instrumental for settling long-standing open problems about the complexity of deciding the existential fragments of Büchi arithmetic and linear arithmetic over p-adic fields. In this article, which accompanies an invited talk, we give a high-level exposition of the NP upper bound for existential Büchi arithmetic, obtain some derived results, and further discuss some open problems.

Type: Proceedings paper
Title: Approaching Arithmetic Theories with Finite-State Automata
Event: 14th International Conference, LATA 2020, Milan, Italy, March 4–6, 2020
Location: Milan
ISBN-13: 978-3-030-40607-3
Open access status: An open access version is available from UCL Discovery
DOI: 10.1007/978-3-030-40608-0_3
Publisher version: https://doi.org/10.1007/978-3-030-40608-0_3
Language: English
Additional information: This is an open access article under the CC BY license (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.
Keywords: Presburger arithmetic, Büchi arithmetic, Reachability ,Automatic structures
UCL classification: UCL
UCL > Provost and Vice Provost Offices
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/10089571
Downloads since deposit
4Downloads
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item