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