Automata theory has come into prominence in recent years with a plethora of applications in fields ranging from verification to XML processing and file compression. In fact, the 2007 Turing Award was awarded to Clarke, Emerson and Sifakis for their pioneering work on model-checking techniques. To the best of our knowledge, there is no single book that covers the vast range of applications of automata theory targeted at a mature student audience. This book is intended to fill that gap and can be used as an intermediate-level textbook. It begins with a detailed treatment of foundational material not normally covered in a beginner's course in automata theory, and then rapidly moves on to applications. The book is largely devoted to verification and model checking, and contains material that is at the cutting edge of verification technology. It will be an invaluable reference for software practitioners working in this area.Contents:Basic Chapters:An Introduction to Finite Automata and Their Connection to Logic (Howard Straubing and Pascal Weil)Finite-State Automata on Infinite Inputs (Madhavan Mukund)Basics on Tree Automata (Christof Löding)An Introduction to Timed Automata (Paritosh K Pandya and P Vijay Suman)Verification:A Language-Theoretic View of Verification (Kamal Lodaya)A Framework for Decentralized Physical Access Control Using Finite State Automata (Namit Chaturvedi, Atish Datta Chowdhury and B Meenakshi)Reasoning about Heap Manipulating Programs Using Automata Techniques (Supratik Chakraborty)Chop Expressions and Discrete Duration Calculus (S Ajesh Babu and Paritosh K Pandya)Automata on Distributed Alphabets (Madhavan Mukund)The Theory of Message Sequence Charts (K Narayan Kumar)Type Checking of Tree Walking Transducers (Sebastian Maneth, Sylvia Friese and Helmut Seidl)Three Case Studies on Verification of Infinite-State Systems (Javier Esparza and Jörg Kreiker)Introduction to Hybrid Automata (Madhu Gopinathan and Pavithra Prabhakar)The Discrete Time Behavior of Restricted Linear Hybrid Automata (Manindra Agrawal, Frank Stephan, P S Thiagarajan and Shaofa Yang)Automata and Logic:Specification and Verification Using Temporal Logics (Stéphane Demri and Paul Gastin)Finite Automata and the Analysis of Infinite Transition Systems (Wolfgang Thomas)Automata Over Infinite Alpahabets (Amaldev Manuel and R Ramanujam)Automata and Logics Over Signals (Fabrice Chevalier, Deepak D'Souza, Raj Mohan M and Pavithra Prabhakar)Compression:Syntax Directed Compression of Trees Using Pushdown Automata (Priti Shankar)Weighted Finite Automata and Digital Images (Kamala Krithivasan and Y Sivasubramanyam)Readership: Computer scientists interested in the practical applications of automata theory; practitioners interested in modern verification techniques.