DIMACS Series in
Discrete Mathematics and Theoretical Computer Science

### Ordering Information

This volume may be obtained from the AMS or through bookstores in your area.

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.

## PREFACE

#### This volume is dedicated to the memory of our colleague and friend Paris C. Kanellakis

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

• (1) the expressive power of logics: studying what can and what cannot be expressed in various logics restricted to finite structures;
• (2) descriptive complexity: studying the logical resources needed to describe queries on finite structures; and
• (3) asymptotic probabilities of logical properties: studying the behavior in the limit of the probability that a large finite structure will satisfy a sentence in a given logic.

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.

### Acknowledgements

We wish to thank the organizers of the Special Year in Logic and Algorithms, Eric Allender, Bob Kurshan, and Moshe Y. Vardi, for organizing and creating a very special year indeed, as well as for entrusting us with the scientific organization and management of the workshop on Finite Models and Descriptive Complexity. We also wish to express our gratitude to Sandy Barbu, the DIMACS coordinator at Princeton University, who took care of the registration and local organization of the workshop in a flawless manner, offering the participants a comfortable, congenial, ideal setting for scientific interactions to take place. (We also felt very lucky that the weather cooperated in that the workshop took place one week after the blizzard of 1996 and one week before a warming trend and heavy rain provided severe flooding.)

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.

#### Dedication

One of the scheduled hour-long talks in the workshop was to be, Computing Over Finite Models = Constraint Databases + Semantics," by Paris C. Kanellakis. We were looking forward to Paris' talk during the workshop and to his survey paper for this volume. Tragically, his life was cut short by an airplane crash in December 1995. In the time slot in which Paris was scheduled to speak a tribute was held to his memory and work. Serge Abiteboul, Gabriel Kuper, and Moshe Y. Vardi, talked about Paris' contributions and reminisced of their collaboration with him. We dedicate this volume to the memory of our colleague and friend Paris C. Kanellakis.

September 1996
Neil Immerman and Phokion G. Kolaitis

Foreword                                                                ix

Preface                                                                 xi

1. Easier Ways to Win Logical Games

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
Contacting the Center