Computation Engineering : Applied Automata Theory and Logic : Applied Automata Theory and Logic - Ganesh Gopalakrishnan

Instant online reading.
Don't wait for delivery!
Go digital and save!

Computation Engineering : Applied Automata Theory and Logic

Applied Automata Theory and Logic

By: Ganesh Gopalakrishnan

Write A Review

Hardcover | 1 June 2006

At a Glance

Hardcover
508 Pages

Dimensions(cm)
23.5 x 15.88 x 3.18

Hardcover

$149.01

or 4 interest-free payments of $37.25 with

Ships in 5 to 7 business days

The computer hardware and software industry is committed to using formal methods. As a result, it is crucial that students who take automata theory and logic courses retain what they have learned and understand how to use their knowledge. Yet many textbooks typically emphasize automata theory only, not logic, thus losing a valuable opportunity to tie these subjects together and reinforce learning. In fact, automata theory and logic evolved hand-in-hand, yet this connection was severed in the '70s as separate automata-theory and logic courses became possible. Now, with computer science departments suffering from overcrowded syllabi, it is often possible for undergraduates to get a BS without having had to take a course in mathematical logic

Today's students want to know how knowledge can work for them -- learning theory as a tool is preferable to learning theory for theory's sake. To prove that theoretical tenents are not only applicable, but also necessary and relevant, useful examples must be presented. This textbook uses interactive tools throughout, such as simple BDD and SAT tools. By providing a blend of theory and practical applications the material is shown to be both inviting and current. Topics are also illustrated in multiple domains so that information is reinforced and students can begin to tie automata theory and logic together. They will also learn multiple uses of fixed-points, including BDD based model checking and understanding context-free productions.

Having used this book, students will not only know and understand automata theory, but also be able to apply their knowledge in real practice.

Industry Reviews

From the reviews:

"One of the constant challenges faced by computer science faculty is how to tie in the theory of computing with applications. This text attempts to do just that ... . Overall, this book is a good undergraduate theory text. ... It includes exercises, with software tools to aid in visualization of key ideas. ... The exercises are appropriate for an undergraduate-level class. ... It is a good text ... ." (M. D. Derk, Computing Reviews, December, 2006)

"The book under review shows, logic and automata theory can be combined to provide powerful tools for checking computer code ... . There is no doubt that the book was written with great care and that it caters for a real need. ... the book is written in a very lively style, which makes reading it quite pleasurable. ... many nice applications of automata that are peppered throughout the book." (S. C. Coutinho, SIGACT News, Vol. 39 (3), 2008)

Shipping

	Standard Shipping	Express Shipping
Metro postcodes:	$9.99	$14.95
Regional postcodes:	$9.99	$14.95
Rural postcodes:	$9.99	$14.95

Orders over $79.00 qualify for free shipping.

How to return your order

At Booktopia, we offer hassle-free returns in accordance with our returns policy. If you wish to return an item, please get in touch with Booktopia Customer Care.

Additional postage charges may be applicable.

Defective items

If there is a problem with any of the items received for your order then the Booktopia Customer Care team is ready to assist you.

For more info please visit our Help Centre.

You Can Find This Book In

Non-Fiction Engineering & Technology Electronics & Communications Engineering Electronics Engineering Circuits & Components Computing & I.T.Computer Programming & Software Development Programming & Scripting Languages Energy Technology & Engineering Electrical Engineering Mathematics Mathematical Foundation

Mathematical Logic Computer Science Mathematical Theory of Computation

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.

Computation Engineering : Applied Automata Theory and Logic

Applied Automata Theory and Logic

At a Glance

Hardcover

Industry Reviews

Shipping

How to return your order

Defective items

You Can Find This Book In

More in Computer Science

Microsoft Power BI For Dummies

For Dummies (Computer/Tech)

Python Crash Course

3rd Edition - A Hands-On, Project-Based Introduction to Programming

The AI Con

How To Fight Big Tech's Hype and Create the Future We Want

The Tech Coup

How to Save Democracy from Silicon Valley

Microsoft 365 Excel For Dummies

For Dummies (Computer/Tech)

The New Age of Sexism

How the AI Revolution is Reinventing Misogyny

Nexus

A Brief History of Information Networks from the Stone Age to AI

Creative Machines

AI, Art & Us

Quantum Gravity and Computation

1st Edition - Information, Pregeometry, and Digital Physics

Microsoft 365 Excel All-in-One For Dummies

Excel for Dummies

Python All-in-One For Dummies

3rd Edition

Empire of AI

Inside the reckless race for total domination

The AI-Driven Leader

Harnessing AI to Make Faster, Smarter Decisions

Artificial Intelligence and Human Rights, Democracy, and the Rule of Law

Computational Intelligence Techniques

Emerging Perspectives and Applications of Computational Intelligence and Smart Systems

Emerging Perspectives and Applications of Computational Intelligence and Smart Systems

Generative Artificial Intelligence

Technology and Applications

Handbook of Smart Manufacturing Technologies

Industrial Engineering in the Digital Age

The Shortest History of AI

Open for Business

Harnessing the Power of Open-Source in the Corporate World

Open for Business

Harnessing the Power of Open-Source in the Corporate World

Operation Carder Kaos

How One Agent Penetrated the Underground Economy

Multidisciplinary Project Management for Organizational Success

Advanced Techniques for Engineering, Science and Management

Driving Intelligence: The Green Book

Routes to Autonomy

This product is categorised by