文档介绍：AUTOMATA-BASED DECISION
PROCEDURES FOR WEAK ARITHMETICS
February 2004
Dissertation zur Erlangung des rades
der Fakult¨at fur¨ Angewandte Wissenschaften
der Albert-Ludwigs-Universit¨at Freiburg im Breisgau
Felix Christopher Klaedtke
******@-
Institut fur¨ Informatik, Albert-Ludwigs-Universitat¨ Freiburg
es-K¨ohler-Allee 52, 79110 Freiburg i. Br., Germany
Dekan: Prof. Dr. Thomas Ottmann
Erstreferent: Prof. Dr. David Basin
Zweitreferent: Prof. Dr. Wolfgang Thomas
Datum der Promotion: 2. Juli 2004
In 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 Wrath
Contents
Acknowledgments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . vii
Zusammenfassung . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ix
Abstract . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . xi
1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1
Motivation, Scope, and Contributions . . . . . . . . . . . . . . . . . . . . . . . . . 1
Standard Notation and Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
Part I: On the Automata Size for Presburger Arithmetic 9
2 Automata Constructions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
Representing Sets of Integers with Automata . . . . . . . . . . . . . . . . . . . 13
Linear Equations and Inequations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
Optimized Constructions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
Divisibility Relation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
Quantifier-Free Formulas . . . . . . .