文件名称：Automata Theory and its Applications
文件大小：8.04MB
文件格式：PDF
更新时间：2021-05-11 02:02:08
Automata
The theory of finite automata on finite stings, infinite strings, and trees has had a distinguished history. First, automata were introduced to represent idealized switching circuits augmented by unit delays. This was the period of Shannon, McCullouch and Pitts, and Howard Aiken, ending about 1950. Then in the 1950s there was the work of Kleene on representable events, of Myhill and Nerode on finite coset congruence relations on strings, of Rabin and Scott on power set automata. In the 1960s, there was the work of Btichi on automata on infinite strings and the second order theory of one successor, then Rabin's 1968 result on automata on infinite trees and the second order theory of two successors. The latter was a mystery until the introduction of forgetful determinacy games by Gurevich and Harrington in 1982. Each of these developments has successful and prospective applications in computer science. They should all be part of every computer scientist's toolbox. Suppose that we take a computer scientist's point of view. One can think of finite automata as the mathematical representation of programs that run using fixed finite resources. Then Btichi's SIS can be thought of as a theory of programs which run forever (like operating systems or banking systems) and are deterministic. Finally, Rabin's S2S is a theory of programs which run forever and are nondeterministic. Indeed many questions of verification can be decided in the decidable theories of these automata. These automata also arise in other languages such as temporal logic and the fL-calculus. Suppose we take a mathematical logician 's point of view. Each of the classes of automata discussed has a corresponding natural decidable theory. As Rabin showed, many theories can be proved decidable by coding them into S2S. Even structures coded into finite automata have proved to be very interesting; witness the theory of automatic groups in topology and the theory of automatic structures. But when the senior author has asked his students to learn these subjects from available textbooks and papers on automata, they have ended up all over the literature trying to put together a coherent exposition. The authors decided to fill this gap with a single self-contained book. This book is a text suitable for a one or two semester course for computer science or mathematics majors, or for a semester graduate course or seminar. The book introduces at the beginning the rudimentary set theory needed, which can be skipped by most readers, advances slowly through the theory of finite automata, and then progresses to the more advanced subjects and some of their applications. We hope that this book will make these beautiful theories available to a larger audience. No advanced mathematical background is required to follow the book. Now we briefly outline the book. The book consists of a bibliography and six chapters titled: • Basic Notions, • Finite Automata, • BUchi Automata, • Games Played on Finite Graphs, • Rabin Automata, • Applications of Rabin Automata. In the first chapter we discuss some basics of rudimentary set theory needed in the book. The chapter can be skipped by most readers. The second chapter is devoted to finite automata. In this chapter we include well-known theorems, The Kleene Theorem and Myhil-Nerode Theorem, which are usually taught in beginning computer science and mathematics courses on computations. We put some topics in this chapter that are usually not covered in the courses. These are finite automata recognizable relations and finite automata with equational constraints. The last section of the chapter is an application of finite automata to logic. The section proves the decidability of the monadic second order logic of finite strings. The third chapter on BUchi automata contains basic results on BUchi automata and BUchi recognizable languages. In this chapter we investigate the relationship between BUchi automata and other types of finite state machines such as MUller automata and sequential Rabin automata. The chapter contains many basic and well-known results about these machines, in particular The McNaughton Theorem. As an application ofBUchi automata we prove the result, first proved by BUchi, that the monadic second order theory of one successor (known as SIS) is decidable. In the fourth chapter we introduce games played on hnite graphs. These games were first studied by McNaughton in the early 1990s, inspired by the work of Gurevich and Harrington on decidability of S2S. The purpose of this chapter is to give a game-theoretic model for concurrent processes of infinite duration and to familiarize the reader with game-theoretic terminology. This chapter introduces the concept of the last visitation record, which plays an important role in proving some fundamental results in this as well as the next chapter. We also introduce and study update games and update networks. The fifth chapter is devoted to Rabin automata. We present the full proof of the complementation problem for Rabin automata by proving that the complement of any Rabin recognizable language is Rabin recognizable. Our proof uses the gametheoretic technique of Gurevich and Harrington. In the chapter we also discuss automata called special automata, and show that these are weaker than Rabin automata. The last chapter contains a series of examples of applications of Rabin automata to mathematical theories. The chapter shows that the following theories are decidable: monadic second order theory of n successors, the monadic second order theory of all countable linearly ordered sets, the monadic second order theory of all countable unary algebras, the theory of Boolean algebras with first order quantifiers and quantifiers over ideals, and theories of structures related to Cantor's discontinuum. All these were first proved by Rabin in his famous 1969 paper. Our bibliography is relatively short, and by no means represents the full range of papers on automata and applications of automata. Therefore, naturally many papers are not included in the bibliography as extensive and updated bibiographies are available on the internet. We also note that there are excellent survey papers on automata in The Handbook of Formal Languages and The Handbook ofTheoretical Computer Science that give extensive bibliographical lists of papers and books on the subject. See for example papers by D. Perrin (Finite Automata), W. Thomas (Languages, Automata, and Logic), and Sheng Yu (Regular Languages). In gathering the bibliography our basic objective was to show the variety of applications of automata to other areas of mathematics and computer science, e.g., algebra, concurrency, complexity, logic, image processing, hybrid systems, networks, probability, programming, real time systems, topology. All the necessary notation and definitions used in this book are introduced in the text. Some proofs of statements (e.g., theorems, lemmas, etc.) are finished with the box 0 sign. This usually means that there is an exercise following that asks the reader to check the correctness of some segments of the proof. Most parts of this book have been taught in graduate and undergraduate courses for mathematics and computer science students at Cornell University, The University of Wisconsin at Madison, The University of Chicago, and partially at Auckland University in New Zealand between 1996 and 2000. We should mention a group of logic graduate students of Cornell University between 1995 and 1999: Jennifer Davoren, Suman Ganguli, Denis Hirschfeldt, Joe Miller, Robert Milnikel, Reed Solomon, and Walker White. Each of them contributed a number of comments and corrections to the text of this book. Suman Ganguli, Denis Hirschfeldt, and Joe Miller put a great effort into the notes of the course and made an enormous number of corrections and suggestions to improve each of the chapters. We thank Richard Shore (Cornell University), Steffen Lempp (The University of Wisconsin at Madison), and Robert Soare (The University of Chicago) who actually attended those graduate courses, made a number of important comments, and discussed the content of the courses. We thank Sasha Rubin, Auckland graduate student, for checking most of the last chapter, Elena Calude from Massey University in New Zealand for reading and commenting on the chapter on Finite Automata. We also thank Michael Dinneen who has been involved in work related to update games and finite automata with equations. We thank Crisian Calude as we benefited from his comments, suggestions and interest in this book. We acknowledge the support of the DOD MURI program, Marsden Fund of New Zealand Royal Society, and the University of Auckland Research Committee. We dedicate this book to our families (parents, wives, sons, and daughters) for their continuing support.