Automata-based decision procedures for weak arithmetics

Around forty years ago, mathematicians such as Büchi and Rabin <br>discovered that automata are a useful mathematical tool for <br>understanding the decidability of different weak systems of <br>arithmetic. A prominent example is the weak monadic second-order logic <br>of one successor, WS1S for short, which is tightly connected to <br>automata over finite words. Nowadays, automata have also emerged as a <br>tool for effectively mechanizing decision procedures for such logical <br>theories. A notable example is Presburger arithmetic for which <br>effective decision procedures can be built using automata. Despite <br>the practical use of automata, many research questions in the <br>automata-based approach to decide weak systems of arithmetic are open. <br>For instance, both lower and upper bounds on the sizes of the automata <br>produced by the automata-based approach for deciding Presburger <br>arithmetic are still unknown. <br> <br>This thesis comprises two parts. In the first part, we analyze the <br>automata-based approach for deciding Presburger arithmetic. We prove <br>that the number of states of the minimal deterministic finite word <br>automaton for a Presburger arithmetic formula is triple exponentially <br>bounded in the length of the formula. This upper bound is established <br>by comparing the automata for Presburger arithmetic formulas with the <br>automata for formulas produced by a quantifier elimination method. We <br>also show that this triple exponential bound is tight. Moreover, we <br>provide optimal automata constructions for linear equations and <br>inequations, and present new techniques for mechanizing an <br>automata-based decision procedure for Presburger arithmetic. <br> <br>In the second part of this thesis, we focus on another system of <br>arithmetic and investigate several decision problems for it. More <br>precisely, we look at WS1S extended with linear cardinality <br>constraints of the form |X_1|+...+|X_r|<|Y_1|+...+|Y_s|, where the <br>X_is and Y_js range over finite sets of natural numbers. We delimit <br>the boundary between decidability and undecidability for WS1S with <br>cardinality constraints. Our investigation is based on the fact that <br>the classical connection between automata and WS1S carries over to a <br>fragment of the extension of WS1S and finite word automata with an <br>extended acceptance condition. The extended acceptance condition is <br>based on a generalization of the commutative image of a word. We <br>identify a decidable fragment of WS1S with cardinality constraints, <br>which non-trivially extends WS1S, and give applications for this <br>decidable fragment.

Author dc:creator

• Klaedtke, Felix

Contributors dc:contributor

• Basin, David

• Presburger-Arithmetik
• monadische Logik zweiter Stufe, WS1S
• Presburger arithmetic
• monadic second-order logic of one successor
• WS1S

Repository record source_url

https://freidok.uni-freiburg.de/data/1439

OAI identifier oai:identifier

oai:freidok.uni-freiburg.de:1439