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 most important result of this part is a new upper complexity bound of <b>NEXPTIME</b> for existential Presburger arithmetic with divisibility. The best bound that was known previously was <b>2NEXPTIME</b>, which followed directly from the original proof of decidability of this theory by Lipshitz in 1976. Lipshitz also gave a proof of <b>NP</b>-hardness of the problem in 1981. Our result is the first improvement of the bound since this original description of a decision procedure. Another new result, which is both an important building block in establishing our new upper complexity bound for existential Presburger arithmetic with divisibility and an interesting result in its own right, is that the decision problem for the existential linear theory of the p-adic numbers is in the Counting Hierarchy <b>CH</b>, and thus within <b>PSPACE</b>. The precise complexity of this problem was stated as open by Weispfenning in 1988, who showed that it is in <b>EXPTIME</b> and <b>NP</b>-hard. The second part of this thesis covers two problems concerning one-counter automata. The first problem is an LTL synthesis problem on one-counter automata with integer-valued and parameterised updates and with equality tests. The decidability of this problem was stated as open by Göller et al. in 2010. We give a reduction of this problem to the decision problem of a subset of Presburger arithmetic with divisibility with one quantifier alternation and a restriction on existentially quantified variables. A proof of decidability of this theory is currently under review. The final result of this thesis concerns a type of one-counter automata that differs from the previous one in that it allows parameters only on tests, not actions, and it includes both equality and disequality tests on counter values. The decidability of the basic reachability problem on such one-counter automata was stated as an open problem by Demri and Sangnier in 2010. We show that this problem is decidable by a reduction to the decision problem for Presburger arithmetic.
| Identifer | oai:union.ndltd.org:bl.uk/oai:ethos.bl.uk:735876 |
| Date | January 2016 |
| Creators | Lechner, Antonia |
| Contributors | Worrell, James |
| Publisher | University of Oxford |
| Source Sets | Ethos UK |
| Detected Language | English |
| Type | Electronic Thesis or Dissertation |
| Source | https://ora.ox.ac.uk/objects/uuid:687bd910-392a-4db0-9fc6-eb10efb8235b |
Page generated in 0.0015 seconds