【文件属性】:
文件名称: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.