To order through AMS contact the AMS Customer Services Department, P.O. Box 6248, Providence, Rhode Island 02940-6248 USA. For Visa, Mastercard, Discover, and American Express orders call 1-800-321-4AMS.
You may also visit the AMS Bookstore and order directly from there. DIMACS does not distribute or sell these books.
Finite model theory can be succinctly described as the study of logics on finite structures. It is an area of research in the interface between mathematical logic and computer science that has been developing through a continuous interaction with computational complexity, database theory, and combinatorics.
Three of the main focuses of research in finite model theory are
These areas are closely coupled. Research in (1) and (2) has amplified the close relationship between logic and computation, as evidenced by natural characterizations of all major complexity classes in terms of logical expressiblility on finite models. Research in (3) has enhanced the synergy between logic and combinatorics, and has led to the discovery of 0-1 laws and convergence laws for various logics on finite structures.
During 1995-96, DIMACS sponsored a Special Year on Logic and Algorithms. The focus areas of this special year were computer aided verification, finite model theory, and proof complexity.
Two of the workshops of the 1995-96 DIMACS Special Year on Logic and Algorithms were devoted to finite model theory. The first was the Workshop on Logic and Random Structures, which took place at Rutgers University, November 5-7, 1995. Its central theme was the relationship between logic and probabilistic techniques in the study of finite structures. The second was the Workshop on Finite Models and Descriptive Complexity, which we organized. It took place at Princeton University, January 14-17, 1996 and was attended by approximately 80 participants.
We had two goals in mind for the Workshop on Finite Models and Descriptive Complexity. The first was to provide a forum for communicating recent advances in the study of expressive power of logics and descriptive complexity, and to bring together researchers from all areas involved in the development of these directions of research. The second was to attempt to create or enhance bridges between finite model theory and related areas, including the other two focus areas of the special year: computer aided verification and proof complexity. State-of-the-art advances in finite model theory and related areas were presented by researchers in 30-minute talks. In addition, we invited a number of researchers to give hour-long talks in which they surveyed a part of finite model theory or presented an overview of another area of research and its potential connections to finite model theory. The program of the workshop with a listing of all talks can be found in pages 246-249 of this volume.
This volume contains seven survey articles by researchers who delivered hour-long talks during the workshop. All seven of these articles are self-contained, readable accounts of research areas connected with finite model theory. They may be read individually in any order and provide valuable introductions to their subjects.
The articles by Ron Fagin and Bruno Courcelle concern expressibility and inexpressibility in monadic, second-order logics. Fagin provides a systematic survey of lower bound techniques using quantifier games. Courcelle focuses on the use of monadic second-order logic as a specification language for graph-theoretic properties. Courcelle's paper provides a bridge between area (1) above and a large and important body of work due to Courcelle and others concerning the complexity of graph properties via monadic second-order logic. Howard Straubing's article lays out the connections between finite model theory, finite automata, and circuit complexity. Victor Vianu's article contains an overview of the interaction between finite model theory and database systems, and also poses a number of challenges to finite model theorists that arise from the current practice of database systems.
The articles by Moshe Y. Vardi and Allen Emerson survey aspects of modal logics of finite Kripke structures, an area of research that provides the underpinnings for computer-aided verification. Vardi's article contains an exposition of complexity results for modal logics with the aim of furnishing explanations for the robust decidability of modal logic and its variants. Emerson provides an introduction and survey of the modal $\mu$-calculus, explaining its applications to verification.
Finally, Toni Pitassi's article presents an overview of recent developments in algebraic proof systems for the propositional calculus, an area of research in proof complexity. Although at present this fascinating area is the least well connected to finite model theory, the connections are palpable. We anticipate that Pitassi's survey will inspire researchers in finite model theory to become involved in proof complexity and thus create further bridges.
Logic has close and deep contacts to all parts of computer science. In the realm of computation all objects being handled and structures being created are finite, or at least finitely describable. While there has been great progress, we have come a very short distance in our ultimate goal of understanding computation. Finite model theory offers a rich, elegant, and rigorous viewpoint, which is interesting in its own right and valuable in its applications to complexity, databases, computer aided verification, as well as many other areas. We hope that this small volume will suggest directions of synergy and contact for future researchers to build upon, creating connections and making discoveries that will help explain some of the many mysteries of computation.
We are grateful to all the participants of the workshop for making the workshop a productive and enlivening event. We thank the authors who contributed articles to this volume. Each of these articles was read by at least two designated readers, who provided comments, corrections, and suggestions to the authors. In many cases, the readers were the editors or the authors of other papers in this volume. In addition, the following colleagues served as readers: P. Beame, S. Buss, S. Cook, O. Kupfermann, C. Lautemann, D. Mix Barrington, and L. Stockmeyer. We thank all the readers for their valuable comments.
Sandy Barbu took the final manuscripts and did the electronic typesetting that produced the book as you see it. We are very grateful indeed to Sandy. Thanks as well to Chris Thivierge of the AMS who handled all remaining aspects of the production of this volume in a very professional, helpful, optimal way.
September 1996
Neil Immerman and Phokion G. Kolaitis
Foreword ix Preface xi 1. Easier Ways to Win Logical Games Ronadl Fagin 1 2. On the Expression of Graph Properties in Some Fragments of Monadic Second-Order Logic Bruno Courcelle 33 3. Finite Models, Automata, and Circuit Complexity Howard Straubing 63 4. Databases and Finite Model Theory Victor Vianu 97 5. Why is Modal Logic so Robustly Decidable? Moshe Y. Vardi 149 6. Model Checking and the Mu-calculus E. Allen Emerson 185 7. Algebraic Propositional Proof Systems Toniann Pitassi 215 8. Program 245
Index of Volumes
DIMACS Homepage