Extensions of Presburger arithmetic and model checking one-counter automata

Thesis

This thesis concerns decision procedures for fragments of linear arithmetic and their application to model-checking one-counter automata. The first part of this thesis covers the complexity of decision problems for different types of linear arithmetic, namely the existential subset of the first-order linear theory over the p-adic numbers and the existential subset of Presburger arithmetic with divisibility, with all integer constants and coefficients represented in binary. The mos...

Expand abstract

Authors: Lechner, A

• Type of award: DPhil
• Level of award: Doctoral
• Awarding institution: University of Oxford
• Language: English
• Keywords: Presburger arithmetic; reachability problems; p-adic numbers; one-counter automata
• Subjects: Computational Complexity Theory; Automata Theory; Linear Arithmetic