Skip to main content
SpringerLink
Log in

Computation Engineering

Applied Automata Theory and Logic

  • Textbook
  • © 2006

Overview

Authors:
  1. Ganesh Gopalakrishnan

    1. Department of Computer Science, University of Utah, Salt Lake City

    View author publications

    You can also search for this author in PubMed   Google Scholar

  • Approaches automata theory and logic as the underlying engineering mathematics for Computation Engineering
  • Covers classical topics such as the Rice's Theorem, as well as modern topics such as Model checking, Buchi Automata, and temporal Logic
  • Restores the Automaton-Logic connection missing in most undergraduate books on automata theory
  • Employs many interactive tools to illustrate key concepts
  • Includes supplementary material: sn.pub/extras

This is a preview of subscription content, log in via an institution to check access.

Access this book

Log in via an institution
eBook USD 89.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 124.00
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book USD 124.00
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

Licence this eBook for your library

Institutional subscriptions

Table of contents (24 chapters)

  1. Front Matter

    Pages I-XXXV
    Download chapter PDF

  2. Introduction

    Pages 1-14

  3. Mathematical Preliminaries

    Pages 15-36

  4. Cardinalities and Diagonalization

    Pages 37-51

  5. Binary Relations

    Pages 53-71

  6. Mathematical Logic, Induction, Proofs

    Pages 73-92

  7. Dealing with Recursion

    Pages 93-104

  8. Strings and Languages

    Pages 105-117

  9. Machines, Languages, DFA

    Pages 119-132

  10. NFA and Regular Expressions

    Pages 133-158

  11. Operations on Regular Machinery

    Pages 159-184

  12. The Automaton/Logic Connection, Symbolic Techniques

    Pages 185-203

  13. The ‘Pumping’ Lemma

    Pages 205-215

  14. Context-free Languages

    Pages 217-244

  15. Push-down Automata and Context-free Grammars

    Pages 245-270

  16. Turing Machines

    Pages 271-290

  17. Basic Undecidability Proofs

    Pages 291-308

  18. Advanced Undecidability Proofs

    Pages 309-321

  19. Basic Notions in Logic including SAT

    Pages 323-344

  20. Complexity Theory and NP-Completeness

    Pages 345-367
Back to top

Keywords

About this book

It takes more e?ort to verify that digital system designs are correct than it does to design them, and as systems get more complex the proportion of cost spent on veri?cation is increasing (one estimate is that veri?cation complexity rises as the square of design complexity). Although this veri?cation crisis was predicted decades ago, it is only recently that powerful methods based on mathematical logic and automata theory have come to the designers’ rescue. The ?rst such method was equivalence checking, which automates Boolean algebra calculations.Nextcamemodelchecking,whichcanautomatically verify that designs have – or don’t have – behaviours of interest speci?ed in temporal logic. Both these methods are available today in tools sold by all the major design automation vendors. It is an amazing fact that ideas like Boolean algebra and modal logic, originating frommathematicians andphilosophersbeforemodern computers were invented, have come to underlie computer aided tools for creating hardware designs. The recent success of ’formal’ approaches to hardware veri?cation has lead to the creation of a new methodology: assertion based design, in which formal properties are incorporated into designs and are then validated by a combination of dynamic simulation and static model checking. Two industrial strength property languages based on tem- ral logic are undergoing IEEE standardisation. It is not only hardwaredesignand veri?cation that is changing: new mathematical approaches to software veri?cation are starting to be - ployed. Microsoft provides windows driver developers with veri?cation tools based on symbolic methods.

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)

Authors and Affiliations

  • Department of Computer Science, University of Utah, Salt Lake City

    Ganesh Gopalakrishnan

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation