Computation engineering: applied automata theory and logic

Contents......Page 7
List of Figures......Page 19
Foreword......Page 25
Preface......Page 27
1 Introduction......Page 37
2.2 Boolean Concepts, Propositions, and Quanti.ers......Page 51
2.3 Sets......Page 52
2.4 Cartesian Product and Powerset......Page 57
2.5 Functions and Signature......Page 58
2.6 The λ Notation......Page 59
2.7 Total, Partial, 1-1, and Onto Functions......Page 61
2.9 Algorithm versus Procedure......Page 63
2.10 Relations......Page 64
2.11 Functions as Relations......Page 66
3.1 Cardinality Basics......Page 73
3.2 The Diagonalization Method......Page 75
3.3 The Schr¨oder-Bernstein Theorem......Page 79
4.1 Binary Relation Basics......Page 89
4.2 Equivalence (Preorder plus Symmetry)......Page 94
4.3 The Power Relation between Machines......Page 97
4.5 Equality, Equivalence, and Congruence......Page 100
5.1 To Prove or Not to Prove!......Page 109
5.2 Proof Methods......Page 111
5.3 Induction Principles......Page 118
5.4 Putting it All Together: the Pigeon-hole Principle......Page 121
6.1 Recursive De.nitions......Page 129
6.2 Recursive De.nitions as Solutions of Equations......Page 133
6.3 Fixed-points in Automata Theory......Page 137
7 Strings and Languages......Page 141
7.1 Strings......Page 142
7.2 Languages......Page 143
8.1 Machines......Page 155
9 NFA and Regular Expressions......Page 169
9.1 What is Nondeterminism?......Page 171
9.2 Regular Expressions......Page 173
9.3 Nondeterministic Finite Automata......Page 177
10.1 NFA to DFA Conversion......Page 195
10.2 Operations on Machines......Page 197
10.3 More Conversions......Page 205
10.4 Error-correcting DFAs......Page 212
10.5 Ultimate Periodicity and DFAs......Page 215
11 The Automaton/Logic Connection, Symbolic Techniques......Page 221
11.1 The Automaton/Logic Connection......Page 222
11.2 Binary Decision Diagrams (BDDs)......Page 223
11.3 Basic Operations on BDDs......Page 227
12.1 Pumping Lemmas for Regular Languages......Page 241
12.2 An adversarial argument......Page 246
12.3 Closure Properties Ameliorate Pumping......Page 247
12.4 Complete Pumping Lemmas......Page 248
13 Context-free Languages......Page 253
13.1 The Language of a CFG......Page 254
13.2 Consistency, Completeness, and Redundancy......Page 256
13.3 Ambiguous......Page 261
13.4 A Taxonomy of Formal Languages and Machines......Page 264
13.5 Push-down Automata......Page 270
13.6 Rightand Left-Linear CFGs......Page 273
13.8 A Pumping Lemma for CFLs......Page 275
14.1 Push-down Automata......Page 281
14.2 Proving PDAs Correct Using Floyd’s Inductive Assertions......Page 289
14.3 Direct Conversion of CFGs to PDAs......Page 290
14.4 Direct Conversion of PDAs to CFGs......Page 293
14.5 The Chomsky Normal Form......Page 298
14.7 Some Important Points Visited......Page 300
15 Turing Machines......Page 307
15.1 Computation: Church/Turing Thesis......Page 308
15.2 Formal De.nition of a Turing machine......Page 309
15.3 Acceptance, Halting, Rejection......Page 314
15.4 Examples......Page 315
15.5 NDTMs......Page 318
15.6 Simulations......Page 322
16 Basic Undecidability Proofs......Page 327
16.1 Some Decidable and Undecidable Problems......Page 328
16.2 Undecidability Proofs......Page 331
17.1 Rice’s Theorem......Page 345
17.2 Failing proof attempt......Page 346
17.3 The Computation History Method......Page 348
18 Basic Notions in Logic including SAT......Page 359
18.1 Axiomatization of Propositional Logic......Page 360
18.2 First-order Logic (FOL) and Validity......Page 362
18.3 Properties of Boolean Formulas......Page 367
19 Complexity Theory and NP-Completeness......Page 381
19.1 Examples and Overview......Page 382
19.2 Formal De.nitions......Page 384
19.3 NPC Theorems and proofs......Page 390
19.4 NP-Hard Problems can be Undecidable (Pitfall)......Page 396
19.5 NP, CoNP, etc.......Page 398
20 DFA for Presburger Arithmetic......Page 405
20.1 Presburger Formulas and DFAs......Page 407
20.2 Pitfalls to Avoid......Page 414
21.1 An Introduction to Model Checking......Page 417
21.2 What Are Reactive Computing Systems?......Page 420
21.3 Buc¨ hi automata, and Verifying Safety and Liveness......Page 425
21.4 Example: Dining Philosophers......Page 426
22.1 Temporal Logics......Page 435
23.1 Enumerative CTL Model Checking......Page 455
23.2 Symbolic Model Checking for CTL......Page 457
23.3 Buc¨ hi Automata and LTL Model Checking......Page 464
23.4 Enumerative Model Checking for LTL......Page 468
24 Conclusions......Page 475
A.2 Software tool usage per chapter......Page 479
A.3 Possible Syllabi......Page 480
B BED Solution to the tic-tac-toe problem......Page 483
References......Page 489
Index......Page 497