{"id":{"repo_id":"freiburg-diss","oai_identifier":"oai:freidok.uni-freiburg.de:1439"},"canonical_url":"https://search.dev.ndltd.org/etd/freiburg-diss/oai:freidok.uni-freiburg.de:1439","repository":{"repo_id":"freiburg-diss","name":"University of Freiburg","base_url":"https://freidok.uni-freiburg.de/oai/oai2.php"},"display":{"title":"Automata-based decision procedures for weak arithmetics","abstract":"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.","abstract_html":"Around forty years ago, mathematicians such as Büchi and Rabin &lt;br&gt;discovered that automata are a useful mathematical tool for &lt;br&gt;understanding the decidability of different weak systems of &lt;br&gt;arithmetic. A prominent example is the weak monadic second-order logic &lt;br&gt;of one successor, WS1S for short, which is tightly connected to &lt;br&gt;automata over finite words. Nowadays, automata have also emerged as a &lt;br&gt;tool for effectively mechanizing decision procedures for such logical &lt;br&gt;theories. A notable example is Presburger arithmetic for which &lt;br&gt;effective decision procedures can be built using automata. Despite &lt;br&gt;the practical use of automata, many research questions in the &lt;br&gt;automata-based approach to decide weak systems of arithmetic are open. &lt;br&gt;For instance, both lower and upper bounds on the sizes of the automata &lt;br&gt;produced by the automata-based approach for deciding Presburger &lt;br&gt;arithmetic are still unknown. &lt;br&gt; &lt;br&gt;This thesis comprises two parts. In the first part, we analyze the &lt;br&gt;automata-based approach for deciding Presburger arithmetic. We prove &lt;br&gt;that the number of states of the minimal deterministic finite word &lt;br&gt;automaton for a Presburger arithmetic formula is triple exponentially &lt;br&gt;bounded in the length of the formula. This upper bound is established &lt;br&gt;by comparing the automata for Presburger arithmetic formulas with the &lt;br&gt;automata for formulas produced by a quantifier elimination method. We &lt;br&gt;also show that this triple exponential bound is tight. Moreover, we &lt;br&gt;provide optimal automata constructions for linear equations and &lt;br&gt;inequations, and present new techniques for mechanizing an &lt;br&gt;automata-based decision procedure for Presburger arithmetic. &lt;br&gt; &lt;br&gt;In the second part of this thesis, we focus on another system of &lt;br&gt;arithmetic and investigate several decision problems for it. More &lt;br&gt;precisely, we look at WS1S extended with linear cardinality &lt;br&gt;constraints of the form |X_1|+...+|X_r|&lt;|Y_1|+...+|Y_s|, where the &lt;br&gt;X_is and Y_js range over finite sets of natural numbers. We delimit &lt;br&gt;the boundary between decidability and undecidability for WS1S with &lt;br&gt;cardinality constraints. Our investigation is based on the fact that &lt;br&gt;the classical connection between automata and WS1S carries over to a &lt;br&gt;fragment of the extension of WS1S and finite word automata with an &lt;br&gt;extended acceptance condition. The extended acceptance condition is &lt;br&gt;based on a generalization of the commutative image of a word. We &lt;br&gt;identify a decidable fragment of WS1S with cardinality constraints, &lt;br&gt;which non-trivially extends WS1S, and give applications for this &lt;br&gt;decidable fragment.","abstract_has_math":false,"creators":["Klaedtke, Felix"],"institution":null,"degree_name":null,"degree_level":null,"degree_discipline":null,"degree_department":null,"school":null,"contributors":["Basin, David"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":null,"date_issued":"","date_published":null,"updated_at":"2026-07-24T02:22:16Z","subjects":["Presburger-Arithmetik","monadische Logik zweiter Stufe, WS1S","Presburger arithmetic","monadic second-order logic of one successor","WS1S"],"languages":[],"rights":[],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"https://freidok.uni-freiburg.de/data/1439","outbound_label":"Repository record","outbound_source":"source_url"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Basin, David"]},{"key":"dc:creator","label":"Author","values":["Klaedtke, Felix"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:type","label":"Dc Type","values":["DoctoralThesis"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Presburger-Arithmetik","monadische Logik zweiter Stufe, WS1S","Presburger arithmetic","monadic second-order logic of one successor","WS1S"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["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.","Mathematiker wie Büchi und Rabin haben vor ungefähr vierzig Jahren <br>entdeckt, dass Automaten ein nützliches mathematisches Werkzeug sind, <br>um die Entscheidbarkeit von bestimmten Teilsystemen der Arithmetik zu <br>verstehen. Ein bedeutendes Beispiel hierfür ist die schwache <br>monadische Logik zweiter Stufe mit einer Nachfolgerfunktion <br>(WS1S). Diese Logik steht in engem Zusammenhang mit Automaten über <br>endlichen Wörtern. Heutzutage werden Automaten auch als Werkzeug <br>eingesetzt, um Entscheidungsprozeduren für solche logischen Theorien <br>umzusetzen. Ein erwähnenswertes Beispiel ist die <br>Presburger-Arithmetik~(PA), für die es leistungsfähige <br>Automaten-basierte Entscheidungsprozeduren gibt. Trotz des hohen <br>praktischen Nutzens von Automaten in diesem Gebiet sind viele <br>Forschungsfragen bezüglich des auf Automaten beruhenden Ansatzes noch <br>unbeantwortet. Ungeklärt sind zum Beispiel sowohl obere als auch <br>untere Schranken für die Größe der Automaten, die bei einer auf <br>Automaten basierenden Entscheidungsprozedur für PA erzeugt werden. <br> <br>Die vorliegende Dissertation gliedert sich in zwei Teile. Im ersten <br>Teil analysieren wir die auf Automaten beruhende Herangehensweise, um <br>PA zu entscheiden. Wir zeigen, dass die Anzahl der Zustände des <br>minimalen, deterministischen, endlichen Automaten dreifach <br>exponentiell in der Länge der PA-Formel beschränkt ist. Wir beweisen <br>die Existenz dieser oberen Schranke dadurch, dass wir die Automaten <br>für PA-Formeln mit den Automaten vergleichen, die wir aus PA-Formeln <br>erhalten, aus denen die Quantoren durch ein <br>Quantoreneliminationsverfahren entfernt wurden. Des Weiteren zeigen <br>wir, dass diese obere, dreifach exponentielle Schranke scharf ist. <br>Darüber hinaus liefern wir optimale Automatenkonstruktionen für <br>lineare Gleichungen und Ungleichungen und präsentieren neue <br>Techniken, die es erlauben, eine auf Automaten basierende <br>Entscheidungsprozedur für PA zu implementieren. <br> <br>Im zweiten Teil der Arbeit betrachten wir ein anderes System der <br>Arithmetik und widmen uns der Untersuchung von mehreren <br>Entscheidbarkeitsfragen darin. Genauer: Wir erweitern WS1S um lineare <br>Kardinalitätsvergleiche der Form <br>|X_1|+...+|X_r|<|Y_1|+...+|Y_s|. Hierbei sind die X_i und Y_i <br>Variablen zweiter Stufe, die durch endliche Mengen natürlicher Zahlen <br>interpretiert werden. Wir zeigen die Grenze zwischen Entscheidbarkeit <br>und Unentscheidbarkeit in diesem System auf. Unsere Untersuchung von <br>Entscheidbarkeitsfragen beruht auf der Übertragung der bekannten <br>Beziehung zwischen WS1S und endlichen Automaten. Wir führen dazu einen <br>neuen Akzpetanzbegriff für Automaten ein, der auf dem kommutativen <br>Bild von Wörtern basiert. Das sich daraus ergebende erweiterte <br>Automatenmodell entspricht hinsichtlich der Ausdrucksmächtigkeit, wie <br>wir zeigen, einem Fragment von WS1S mit Kardinalitätsvergleichen. <br>Schließlich beweisen wir die Entscheidbarkeit eines Fragments von WS1S <br>mit Kardinalitätsvergleichen und zeigen Anwendungen für eben dieses <br>Fragment auf."]},{"key":"dc:format.medium","label":"Dc Format Medium","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Automata-based decision procedures for weak arithmetics","Automaten-basierende Entscheidungsverfahren für schwache Arithmetik"]}]}],"canonical_facts":{"dc:contributor":["Basin, David"],"dc:creator":["Klaedtke, Felix"],"dc:description.abstract":["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.","Mathematiker wie Büchi und Rabin haben vor ungefähr vierzig Jahren <br>entdeckt, dass Automaten ein nützliches mathematisches Werkzeug sind, <br>um die Entscheidbarkeit von bestimmten Teilsystemen der Arithmetik zu <br>verstehen. Ein bedeutendes Beispiel hierfür ist die schwache <br>monadische Logik zweiter Stufe mit einer Nachfolgerfunktion <br>(WS1S). Diese Logik steht in engem Zusammenhang mit Automaten über <br>endlichen Wörtern. Heutzutage werden Automaten auch als Werkzeug <br>eingesetzt, um Entscheidungsprozeduren für solche logischen Theorien <br>umzusetzen. Ein erwähnenswertes Beispiel ist die <br>Presburger-Arithmetik~(PA), für die es leistungsfähige <br>Automaten-basierte Entscheidungsprozeduren gibt. Trotz des hohen <br>praktischen Nutzens von Automaten in diesem Gebiet sind viele <br>Forschungsfragen bezüglich des auf Automaten beruhenden Ansatzes noch <br>unbeantwortet. Ungeklärt sind zum Beispiel sowohl obere als auch <br>untere Schranken für die Größe der Automaten, die bei einer auf <br>Automaten basierenden Entscheidungsprozedur für PA erzeugt werden. <br> <br>Die vorliegende Dissertation gliedert sich in zwei Teile. Im ersten <br>Teil analysieren wir die auf Automaten beruhende Herangehensweise, um <br>PA zu entscheiden. Wir zeigen, dass die Anzahl der Zustände des <br>minimalen, deterministischen, endlichen Automaten dreifach <br>exponentiell in der Länge der PA-Formel beschränkt ist. Wir beweisen <br>die Existenz dieser oberen Schranke dadurch, dass wir die Automaten <br>für PA-Formeln mit den Automaten vergleichen, die wir aus PA-Formeln <br>erhalten, aus denen die Quantoren durch ein <br>Quantoreneliminationsverfahren entfernt wurden. Des Weiteren zeigen <br>wir, dass diese obere, dreifach exponentielle Schranke scharf ist. <br>Darüber hinaus liefern wir optimale Automatenkonstruktionen für <br>lineare Gleichungen und Ungleichungen und präsentieren neue <br>Techniken, die es erlauben, eine auf Automaten basierende <br>Entscheidungsprozedur für PA zu implementieren. <br> <br>Im zweiten Teil der Arbeit betrachten wir ein anderes System der <br>Arithmetik und widmen uns der Untersuchung von mehreren <br>Entscheidbarkeitsfragen darin. Genauer: Wir erweitern WS1S um lineare <br>Kardinalitätsvergleiche der Form <br>|X_1|+...+|X_r|<|Y_1|+...+|Y_s|. Hierbei sind die X_i und Y_i <br>Variablen zweiter Stufe, die durch endliche Mengen natürlicher Zahlen <br>interpretiert werden. Wir zeigen die Grenze zwischen Entscheidbarkeit <br>und Unentscheidbarkeit in diesem System auf. Unsere Untersuchung von <br>Entscheidbarkeitsfragen beruht auf der Übertragung der bekannten <br>Beziehung zwischen WS1S und endlichen Automaten. Wir führen dazu einen <br>neuen Akzpetanzbegriff für Automaten ein, der auf dem kommutativen <br>Bild von Wörtern basiert. Das sich daraus ergebende erweiterte <br>Automatenmodell entspricht hinsichtlich der Ausdrucksmächtigkeit, wie <br>wir zeigen, einem Fragment von WS1S mit Kardinalitätsvergleichen. <br>Schließlich beweisen wir die Entscheidbarkeit eines Fragments von WS1S <br>mit Kardinalitätsvergleichen und zeigen Anwendungen für eben dieses <br>Fragment auf."],"dc:format.medium":["application/pdf"],"dc:subject":["Presburger-Arithmetik","monadische Logik zweiter Stufe, WS1S","Presburger arithmetic","monadic second-order logic of one successor","WS1S"],"dc:title":["Automata-based decision procedures for weak arithmetics","Automaten-basierende Entscheidungsverfahren für schwache Arithmetik"],"dc:type":["DoctoralThesis"]},"updated_at":"2026-07-24T02:22:16Z"}