Automata-based decision procedures for weak arithmetics [Elektronische Ressource] / Felix Christopher Klaedtke

Sujets

• Informatik
• Mathematics

Informations

• Publié par: albert-ludwigs-universitat_freiburg
• Publié le: 01 janvier 2004
• Nombre de lectures: 55
• Langue: English
• Poids de l'ouvrage: 1 Mo

Extrait

AUTOMATA-BASED DECISION
PROCEDURES FOR WEAK ARITHMETICS
February 2004
Dissertation zur Erlangung des Doktorgrades
der Fakult at fur Angewandte Wissenschaften
der Albert-Ludwigs-Universit at Freiburg im Breisgau
Felix Christopher Klaedtke
[e-mail]
Institut fur Informatik, Albert-Ludwigs-Universitat Freiburg
Georges-K ohler-Allee 52, 79110 Freiburg i. Br., GermanyDekan: Prof. Dr. Thomas Ottmann
Erstreferent: Prof. Dr. David Basin
Zweitreferent: Prof. Dr. Wolfgang Thomas
Datum der Promotion: 2. Juli 2004In memory of Alexander Schneider
\Well, don’ tell ’em. Go down the river an’ stick
your head under an’ whisper ’em in the stream."
| Steinbeck, The Grapes of WrathContents
Acknowledgments ::::::::::::::::::::::::::::::::::::::::::::::: vii
Zusammenfassung ::::::::::::::::::::::::::::::::::::::::::::::: ix
Abstract::::::::::::::::::::::::::::::::::::::::::::::::::::::::: xi
1 Introduction ::::::::::::::::::::::::::::::::::::::::::::::::: 1
1.1 Motivation, Scope, and Contributions . . . . . . . . . . . . . . . . . . . . . . . . . 1
1.2 Standard Notation and De nitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
Part I: On the Automata Size for Presburger Arithmetic 9
2 Automata Constructions ::::::::::::::::::::::::::::::::::::: 13
2.1 Representing Sets of Integers with Automata . . . . . . . . . . . . . . . . . . . 13
2.2 Linear Equations and Inequations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
2.3 Optimized Constructions. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
2.4 Divisibility Relation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
2.5 Quanti er-F ree Formulas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
3 Upper Bound on the Automata Size ::::::::::::::::::::::::: 25
3.1 Eliminating a Quanti er in Presburger Arithmetic . . . . . . . . . . . . . . 25
3.2 Analysis of Eliminating a Quanti er . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
3.3 Quanti er Elimination for Arbitrary Formulas . . . . . . . . . . . . . . . . . . 32
3.4 Putting It Together . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
4 A Worst Case Example :::::::::::::::::::::::::::::::::::::: 41
5 Mechanization ::::::::::::::::::::::::::::::::::::::::::::::: 45
5.1 Data-Structures for Automata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
5.2 Automata Construction for Linear Equations . . . . . . . . . . . . . . . . . . . 52
5.3 Improved Product Construction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61
5.4 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71
6 Concluding Remarks and Future Work::::::::::::::::::::::: 73
6.1 Other Representations of Integers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73
6.2 Automata-Based Decision Procedures . . . . . . . . . . . . . . . . . . . . . . . . . 75
Part II: WS1S with Cardinality Constraints 77
7 Parikh Automata :::::::::::::::::::::::::::::::::::::::::::: 79
7.1 Arithmetical Constraint Languages . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79
7.2 Comparison to Other Automata Models . . . . . . . . . . . . . . . . . . . . . . . 80
7.3 Closure Properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82
7.4 Decision Problems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84vi Contents
8 Extension of the Classical Automata-Logic Connection::::::: 87
8.1 WS1S with Cardinality Constraints . . . . . . . . . . . . . . . . . . . . . . . . . . . 87
card8.2 Parikh Automata and WS1S . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 89
8.3 Undecidability and Decidability Results . . . . . . . . . . . . . . . . . . . . . . . . 92
8.4 Generalization to Trees . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 96
9 Applications ::::::::::::::::::::::::::::::::::::::::::::::::: 101
9.1 Implementation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101
9.2 Case Studies . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 112
10 Conclusion:::::::::::::::::::::::::::::::::::::::::::::::::: 121
Appendix
11 Some Standard De nitions :::::::::::::::::::::::::::::::::: 125
11.1 Binary Decision Diagrams. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 125
11.2 Register Machines. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 126
12 Additional Proof Details in Part I::::::::::::::::::::::::::: 127
12.1 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 127
12.2 The Proof. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 128
13 Additional Proof Details in Part II:::::::::::::::::::::::::: 133
13.1 Comparison of PWAs to Other Automata Models . . . . . . . . . . . . . . . 133
13.2 Closure Properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 140
card13.3 Petri Net Reachability Problem in WS1S . . . . . . . . . . . . . . . . . . . 144
13.4 Linear Polynomial Cover . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 146
14 Listings ::::::::::::::::::::::::::::::::::::::::::::::::::::: 149
14.1 Lemmas about Cardinalities of Finite Sets . . . . . . . . . . . . . . . . . . . . . 149
14.2 Dining Philosophers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 151
14.3 A Planning Problem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 153
14.4 D-type Flip- op . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 154
Literature ::::::::::::::::::::::::::::::::::::::::::::::::::::::: 157
Symbol Index:::::::::::::::::::::::::::::::::::::::::::::::::::: 165
Index:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 167Acknowledgments
irst, I want to thank my supervisor, David Basin, for guiding me and
for providing me the space and the support to pursue my ideas and interests.
I owe him much of my education, the work I present in this thesis, and the
scienti c work I may do in the future. Thanks a lot!
I want to thank Rafael Accorsi for his support and patience and continuous
helpfulness. I also want to thank all the other group members (present and
past) in Freiburg for their support and for providing a pleasant and productive
working atmosphere: Abdelwaheb Ayari, Achim Brucker, Burkhart Wol , Erika
Abrah am, Frank Rittinger, Georg Struth, Ina Eckert, Jan-Georg Smaus, Jurgen
Doser, Luca Vigan o, Marlis Jost, Martin Preen, Sabine Bennemann, Sebastian
M odersheim, Stefan Friedrich, and Torsten Lodderstedt. Many thanks to the
people at SRI, in particular Jose Meseguer and Harald Rue with whom I had
the chance to work with.
I want to thank the \Firenze" companions Achim Brucker, Dirk Bockhorn,
Kristian Kersting, Marc Herbstritt, Noe Spinner, and Tobias Schubert for their
support and the enjoyable discussions about life, politics, computer science, and
all that. Thanks also to Marco Ho mann, Michael Brenner, Robert Ritter, Silvia
Fritz, Till Nachtmann, and Tobias Grimminger for many things.
Finally and foremost, I want to thank my parents for their true and unlimited
love.
Felix Klaedtke
Freiburg i. Br., Germany
February 13, 2004
viiZusammenfassung
Mathematiker wie Buc hi und Rabin haben vor ungef ahr vierzig Jahren ent-
deckt, dass Automaten ein nutzlic hes mathematisches Werkzeug sind, um die
Entscheidbarkeit von bestimmten Teilsystemen der Arithmetik zu verstehen. Ein
bedeutendes Beispiel hierfur ist die schwache monadische Logik zweiter Stufe mit
einer Nachfolgerfunktion (WS1S). Diese Logik steht in engem Zusammenhang
mit Automaten ub er endlichen W ortern. Heutzutage werden Automaten auch als
Werkzeug eingesetzt, um Entscheidungsprozeduren fur solche logischen Theorien
umzusetzen. Ein erw ahnenswertes Beispiel ist die Presburger-Arithmetik (PA),
fur die es leistungsf ahige Automaten-basierte Entscheidungsprozeduren gibt.
Trotz des hohen praktischen Nutzens von Automaten in diesem Gebiet sind viele
Forschungsfragen bezuglic h des auf Automaten beruhenden Ansatzes noch un-
beantwortet. Ungekl art sind zum Beispiel sowohl obere als auch untere Schranken
fur die Gr o e der Automaten, die bei einer auf Automaten basierenden Entscheid-
ungsprozedur fur PA erzeugt werden.
Die vorliegende Dissertation gliedert sich in zwei Teile. Im ersten Teil ana-
lysieren wir die auf Automaten beruhende Herangehensweise, um PA zu entschei-
den. Wir zeigen, dass die Anzahl der Zust ande des minimalen, deterministischen,
endlichen Automaten dreifach exponentiell in der L ange der PA-Formel be-
schr ankt ist. Wir beweisen die Existenz dieser oberen Schranke dadurch, dass wir
die Automaten fur PA-Formeln mit den Automaten vergleichen, die wir aus PA-
Formeln erhalten, aus denen die Quantoren durch ein Quantoreneliminationsver-
fahren entfernt wurden. Des Weiteren zeigen wir, dass diese obere, dreifach expo-
nentielle Schranke scharf ist. Darub er hinaus liefern wir optimale Automatenkon-
struktionen fur