Foreword | p. XXV |
Preface | p. XXVII |
Introduction | p. 1 |
Computation Science and Computation Engineering | p. 1 |
What is 'Computation?' | p. 2 |
A Minimalist Approach | p. 3 |
How to Measure the Power of Computers? | p. 5 |
Complexity Theory | p. 5 |
Automata Theory and Computing | p. 6 |
Why "Mix-up" Automata and Mathematical Logic? | p. 7 |
Why Verify? Aren't Computers "Mostly Okay?" | p. 7 |
Verifying Computing Systems Using Automaton Models | p. 9 |
Automaton/Logic Connection | p. 10 |
Avoid Attempting the Impossible | p. 11 |
Solving One Implies Solving All | p. 11 |
Automata Theory Demands a Lot From You! | p. 12 |
A Brief Foray Into History | p. 12 |
Disappearing Formal Methods | p. 13 |
Exercises | p. 14 |
Mathematical Preliminaries | p. 15 |
Numbers | p. 15 |
Boolean Concepts, Propositions, and Quantifiers | p. 15 |
Sets | p. 16 |
Defining sets | p. 16 |
Avoid contradictions | p. 17 |
Ensuring uniqueness of definitions | p. 18 |
Cartesian Product and Powerset | p. 21 |
Powersets and characteristic sequences | p. 22 |
Functions and Signature | p. 22 |
The [lambda] Notation | p. 23 |
Total, Partial, 1-1, and Onto Functions | p. 25 |
Computable Functions | p. 27 |
Algorithm versus Procedure | p. 27 |
Relations | p. 28 |
Functions as Relations | p. 30 |
More [lambda] syntax | p. 30 |
Exercises | p. 31 |
Cardinalities and Diagonalization | p. 37 |
Cardinality Basics | p. 37 |
Countable sets | p. 38 |
Cardinal numbers | p. 38 |
Cardinality "trap" | p. 39 |
The Diagonalization Method | p. 39 |
Simplify the set in question | p. 40 |
Avoid dual representations for numbers | p. 40 |
Claiming a bijection, and refuting it | p. 41 |
'Fixing' the proof a little bit | p. 41 |
Cardinality of 2[superscript Nat] and Nat [right arrow] Bool | p. 43 |
The Schroder-Bernstein Theorem | p. 43 |
Application: cardinality of all C Programs | p. 44 |
Application: functions in Nat [right arrow] Bool | p. 44 |
Proof of the Schroder-Bernstein Theorem | p. 46 |
Exercises | p. 50 |
Binary Relations | p. 53 |
Binary Relation Basics | p. 53 |
Types of binary relations | p. 54 |
Preorder (reflexive plus transitive) | p. 57 |
Partial order (preorder plus antisymmetric) | p. 57 |
Total order, and related notions | p. 58 |
Equivalence (Preorder plus Symmetry) | p. 58 |
Intersecting a preorder and its inverse | p. 59 |
Identity relation | p. 59 |
Universal relation | p. 59 |
Equivalence class | p. 60 |
Reflexive and transitive closure | p. 60 |
The Power Relation between Machines | p. 61 |
The equivalence relation over machine types | p. 62 |
Lattice of All Binary Relations over S | p. 64 |
Equality, Equivalence, and Congruence | p. 64 |
Congruence relation | p. 64 |
Exercises | p. 67 |
Mathematical Logic, Induction, Proofs | p. 73 |
To Prove or Not to Prove! | p. 73 |
Proof Methods | p. 75 |
The implication operation | p. 75 |
'If,' or 'Definitional Equality' | p. 76 |
Proof by contradiction | p. 77 |
Quantification operators [for all] and [exists] | p. 78 |
Generalized DeMorgan's Law Relating [for all] And [exists] | p. 80 |
Inductive definitions of sets and functions | p. 80 |
Induction Principles | p. 82 |
Induction over natural numbers | p. 82 |
Noetherian induction | p. 84 |
Structural | p. 85 |
Putting it All Together: the Pigeon-hole Principle | p. 85 |
Exercises | p. 86 |
Dealing with Recursion | p. 93 |
Recursive Definitions | p. 93 |
Recursion viewed as solving for a function | p. 94 |
Fixed-point equations | p. 95 |
The Y operator | p. 96 |
Illustration of reduction | p. 97 |
Recursive Definitions as Solutions of Equations | p. 97 |
The least fixed-point | p. 100 |
Fixed-points in Automata Theory | p. 101 |
Exercises | p. 103 |
Strings and Languages | p. 105 |
Strings | p. 106 |
The empty string [epsilon] | p. 106 |
Length, character at index, and substring of a string | p. 107 |
Concatenation of strings | p. 107 |
Languages | p. 107 |
How many languages are there? | p. 108 |
Orders for Strings | p. 108 |
Operations on languages | p. 110 |
Concatenation and exponentiation | p. 110 |
Kleene Star, '*' | p. 112 |
Complementation | p. 112 |
Reversal | p. 113 |
Homomorphism | p. 113 |
Ensuring homomorphisms | p. 113 |
Inverse homomorphism | p. 114 |
An Illustration of homomorphisms | p. 115 |
Prefix-closure | p. 115 |
Exercises | p. 116 |
Machines, Languages, DFA | p. 119 |
Machines | p. 119 |
The DFA | p. 121 |
The "power" of DFAs | p. 126 |
Limitations of DFAs | p. 126 |
Machine types that accept non-regular languages | p. 127 |
Drawing DFAs neatly | p. 129 |
Exercises | p. 130 |
NFA and Regular Expressions | p. 133 |
What is Nondeterminism? | p. 135 |
How nondeterminism affects automaton operations | p. 136 |
How nondeterminism affects the power of machines | p. 137 |
Regular Expressions | p. 137 |
Nondeterministic Finite Automata | p. 141 |
Nondeterministic Behavior Without [epsilon] | p. 141 |
Nondeterministic behavior with [epsilon] | p. 143 |
Eclosure (also known as [epsilon]-closure) | p. 145 |
Language of an NFA | p. 147 |
A detailed example: telephone numbers | p. 149 |
Tool-assisted study of NFAs, DFAs, and REs | p. 151 |
Exercises | p. 157 |
Operations on Regular Machinery | p. 159 |
NFA to DFA Conversion | p. 159 |
Operations on Machines | p. 161 |
Union | p. 162 |
Intersection | p. 165 |
Complementation | p. 165 |
Concatenation | p. 165 |
Star | p. 166 |
Reversal | p. 167 |
Homomorphism | p. 168 |
Inverse Homomorphism | p. 168 |
Prefix-closure | p. 169 |
More Conversions | p. 169 |
RE to NFA | p. 169 |
NFA to RE | p. 170 |
Minimizing DFA | p. 174 |
Error-correcting DFAs | p. 176 |
DFA constructed using error strata | p. 177 |
DFA constructed through regular expressions | p. 177 |
Ultimate Periodicity and DFAs | p. 179 |
Exercises | p. 181 |
The Automaton/Logic Connection, Symbolic Techniques | p. 185 |
The Automaton/Logic Connection | p. 186 |
DFA can 'scan' and also 'do logic' | p. 186 |
Binary Decision Diagrams (BDDs) | p. 187 |
Basic Operations on BDDs | p. 191 |
Representing state transition systems | p. 192 |
Forward reachability | p. 193 |
Fixed-point iteration to compute the least fixed-point | p. 194 |
An example with multiple fixed-points | p. 197 |
Playing tic-tac-toe using BDDs | p. 198 |
Exercises | p. 200 |
The 'Pumping' Lemma | p. 205 |
Pumping Lemmas for Regular Languages | p. 205 |
A stronger incomplete Pumping Lemma | p. 209 |
An adversarial argument | p. 210 |
Closure Properties Ameliorate Pumping | p. 211 |
Complete Pumping Lemmas | p. 212 |
Jaffe's complete Pumping Lemma | p. 212 |
Stanat and Weiss' complete Pumping Lemma | p. 213 |
Exercises | p. 213 |
Context-free Languages | p. 217 |
The Language of a CFG | p. 218 |
Consistency, Completeness, and Redundancy | p. 220 |
More consistency proofs | p. 223 |
Fixed-points again! | p. 224 |
Ambiguous Grammars | p. 225 |
If-then-else ambiguity | p. 226 |
Ambiguity, inherent ambiguity | p. 227 |
A Taxonomy of Formal Languages and Machines | p. 228 |
Non-closure of CFLs under complementation | p. 230 |
Simplifying CFGs | p. 232 |
Push-down Automata | p. 234 |
DPDA versus NPDA | p. 235 |
Deterministic context-free languages (DCFL) | p. 235 |
Some Factoids | p. 236 |
Right- and Left-Linear CFGs | p. 237 |
Developing CFGs | p. 239 |
A Pumping Lemma for CFLs | p. 239 |
Exercises | p. 242 |
Push-down Automata and Context-free Grammars | p. 245 |
Push-down Automata | p. 245 |
Conventions for describing PDAs | p. 247 |
Acceptance by final state | p. 247 |
Acceptance by empty stack | p. 249 |
Conversion of P[subscript 1] to P[subscript 2] ensuring L(P[subscript 1]) = N (P[subscript 2]) | p. 251 |
Conversion of P[subscript 1] to P[subscript 2] ensuring N(P[subscript 1]) = L(P[subscript 2]) | p. 251 |
Proving PDAs Correct Using Floyd's Inductive Assertions | p. 253 |
Direct Conversion of CFGs to PDAs | p. 254 |
Direct Conversion of PDAs to CFGs | p. 257 |
Name non-terminals to match stack-emptying possibilities | p. 258 |
Let start symbol S set up all stack-draining options | p. 258 |
Capture how each PDA transition helps drain the stack | p. 259 |
Final result from Figure 14.6 | p. 260 |
The Chomsky Normal Form | p. 262 |
Cocke-Kasami-Younger (CKY) parsing algorithm | p. 262 |
Closure and Decidability | p. 264 |
Some Important Points Visited | p. 264 |
Chapter Summary - Lost Venus Probe | p. 267 |
Exercises | p. 268 |
Turing Machines | p. 271 |
Computation: Church/Turing Thesis | p. 272 |
"Turing machines" according to Turing | p. 273 |
Formal Definition of a Turing machine | p. 273 |
Singly- or doubly-infinite tape? | p. 275 |
Two stacks+control = Turing machine | p. 276 |
Linear bounded automata | p. 277 |
Tape vs. random access memory | p. 278 |
Acceptance, Halting, Rejection | p. 278 |
"Acceptance" of a TM closely examined | p. 278 |
Instantaneous descriptions | p. 279 |
Examples | p. 279 |
Examples illustrating TM concepts and conventions | p. 280 |
A DTM for w#w | p. 282 |
NDTMs | p. 282 |
Guess and check | p. 283 |
An NDTM for ww | p. 286 |
Simulations | p. 286 |
Multi-tape vs. single-tape Turing machines | p. 286 |
Nondeterministic Turing machines | p. 286 |
The Simulation itself | p. 287 |
Exercises | p. 288 |
Basic Undecidability Proofs | p. 291 |
Some Decidable and Undecidable Problems | p. 292 |
An assortment of decidable problems | p. 292 |
Assorted undecidable problems | p. 294 |
Undecidability Proofs | p. 295 |
Turing recognizable (or recursively enumerable) sets | p. 295 |
Recursive (or decidable) languages | p. 297 |
Acceptance (A[subscript TM]) is undecidable (important!) | p. 298 |
Halting (Halt[subscript TM]) is undecidable (important!) | p. 299 |
Mapping reductions | p. 301 |
Undecidable problems are "A[subscript TM] in disguise" | p. 305 |
Exercises | p. 306 |
Advanced Undecidability Proofs | p. 309 |
Rice's Theorem | p. 309 |
Failing proof attempt | p. 310 |
Corrected proof | p. 311 |
Greibach's Theorem | p. 312 |
The Computation History Method | p. 312 |
Decidability of LBA acceptance | p. 313 |
Undecidability of LBA language emptiness | p. 313 |
Undecidability of PDA language universality | p. 313 |
Post's correspondence problem (PCP) | p. 315 |
PCP is undecidable | p. 316 |
Proof sketch of the undecidability of PCP | p. 317 |
Exercises | p. 320 |
Basic Notions in Logic including SAT | p. 323 |
Axiomatization of Propositional Logic | p. 324 |
First-order Logic (FOL) and Validity | p. 326 |
A warm-up exercise | p. 326 |
Examples of interpretations | p. 327 |
Validity of first-order logic is undecidable | p. 329 |
Valid FOL formulas are enumerable | p. 331 |
Properties of Boolean Formulas | p. 331 |
Boolean satisfiability: an overview | p. 331 |
Normal forms | p. 332 |
Overview of direct DNF to CNF conversion | p. 333 |
CNF-conversion using gates | p. 336 |
DIMACS file encoding | p. 337 |
Unsatisfiable CNF instances | p. 339 |
3-CNF, [not equal]-satisfiability, and general CNF | p. 340 |
2-CNF satisfiability | p. 341 |
Exercises | p. 342 |
Complexity Theory and NP-Completeness | p. 345 |
Examples and Overview | p. 346 |
The traveling salesperson problem | p. 346 |
P-time deciders, robustness, and 2 vs. 3 | p. 346 |
A note on complexity measurement | p. 347 |
The robustness of the Turing machine model | p. 348 |
Going from "2 to 3" changes complexity | p. 348 |
Formal Definitions | p. 348 |
NP viewed in terms of verifiers | p. 348 |
Some problems are outside NP | p. 349 |
NP-complete and NP-hard | p. 350 |
NP viewed in terms of deciders | p. 350 |
An example of an NP decider | p. 351 |
Minimal input encodings | p. 353 |
NPC Theorems and proofs | p. 353 |
NP-Completeness of 3-SAT | p. 354 |
Practical approaches to show NPC | p. 358 |
NP-Hard Problems can be Undecidable (Pitfall) | p. 360 |
Proof that Diophantine Equations are NPH | p. 360 |
"Certificates" of Diophantine Equations | p. 361 |
What other complexity measures exist? | p. 362 |
NP, CoNP, etc. | p. 362 |
Exercises | p. 365 |
DFA for Presburger Arithmetic | p. 369 |
Presburger Formulas and DFAs | p. 371 |
Presburger formulas | p. 371 |
Encoding conventions | p. 373 |
Example 1 - representing x [less than equal to] 2 | p. 373 |
Example 2 - [for all]x.[exists]y.(x + y) = 1 | p. 375 |
Conversion algorithm: Presburger formulas to automata | p. 376 |
Pitfalls to Avoid | p. 378 |
The restriction of equal bit-vector lengths | p. 379 |
Exercises | p. 380 |
Model Checking: Basics | p. 381 |
An Introduction to Model Checking | p. 381 |
What Are Reactive Computing Systems? | p. 384 |
Why model checking? | p. 385 |
Model checking vs. testing | p. 387 |
Buchi automata, and Verifying Safety and Liveness | p. 389 |
Example: Dining Philosophers | p. 390 |
Model (proctype) and property (never) automata | p. 394 |
Exercises | p. 396 |
Model Checking: Temporal Logics | p. 399 |
Temporal Logics | p. 399 |
Kripke structures | p. 399 |
Computations vs. computation trees | p. 401 |
Temporal formulas are Kripke structure classifiers! | p. 403 |
LTL vs. CTL through an example | p. 405 |
LTL syntax | p. 406 |
LTL semantics | p. 406 |
CTL syntax | p. 407 |
CTL semantics | p. 408 |
Exercises | p. 414 |
Model Checking: Algorithms | p. 419 |
Enumerative CTL Model Checking | p. 419 |
Symbolic Model Checking for CTL | p. 421 |
EG p through fixed-point iteration | p. 421 |
Calculating EX and AX | p. 424 |
LFP and GFP for 'Until' | p. 425 |
LFP for 'Until' | p. 426 |
GFP for Until | p. 427 |
Buchi Automata and LTL Model Checking | p. 428 |
Comparing expressiveness | p. 428 |
Operations on Buchi automata | p. 430 |
Nondeterminism in Buchi automata | p. 431 |
Enumerative Model Checking for LTL | p. 432 |
Reducing verification to Buchi automaton emptiness | p. 433 |
Exercises | p. 436 |
Conclusions | p. 439 |
Book web site and tool information | p. 443 |
Web site and e-mail address | p. 443 |
Software tool usage per chapter | p. 443 |
Possible Syllabi | p. 444 |
BED Solution to the tic-tac-toe problem | p. 447 |
References | p. 453 |
Index | p. 461 |
Table of Contents provided by Ingram. All Rights Reserved. |