Major Research Accomplishments#
Logical Theory of Databases: Database management systems are evolving from unsophisticated databases, which are essentially structured collections of data, toward “smart” databases possessing deductive capabilities. The line between databases and knowledge bases is becoming less and less clear. I have investigated the logical theory of databases, with a focus on the trade-off between expressiveness and computational complexity. My research laid the foundations in the following areas: integrity constraints, complexity of query evaluation, incomplete information, database updates, and information integration.
Reasoning about Knowledge: Reasoning about knowledge has found applications in such diverse fields as economics, linguistics, artificial intelligence and computer science. For example, a robot in a system may have to know what other robots know in order to coordinate a plan. Similarly, in a bargaining session, side A may need to reason about what side B knows (and what side B knows about what side A knows, and so on) in order to bargain effectively. Together with Halpern and Fagin, I developed an extensive theory of reasoning about knowledge. This work focuses on (a) using reasoning about knowledge to design, analyze and verify the correctness of distributed systems, and (b) providing good formal models of knowledge that are appropriate for various applications.
In addition to pursuing this research, Fagin, Halpern and I initiated and organized an interdisciplinary conference on the subject. The conference (“Theoretical Aspects of Reasoning about Knowledge”), which brings together researchers from diverse fields, such as AI, game theory, philosophy, and distributed systems, met biannually since 1986. This work was recognized as one of the top accomplishments of the IBM Almaden Research Center in 1985, and won an IBM Outstanding Innovation Award in 1987. A book titled “Reasoning about Knowledge” by Fagin, Halpern, Moses, and myself, was published by MIT Press in 1995.
An Automata-Theoretic Approach to Concurrent Program Verification: I have demonstrated that questions about correctness of concurrent programs can be reduced to questions about finite automata on infinitary input structures (infinite words or infinite trees). Carrying out this approach required advances in both automata theory and the theory of program logics. This connection brought a wealth of new techniques to the theory of program logic, and the new application revived the theory of automata on infinitary inputs. The work has several potential software engineering applications; a particularly important application concerns automatic verification of finite-state protocols, such as communication protocols. This work serves as the basis of several automated verification tools, such as Lucent’s FormalCheck, SDLVALID, and SPIN, and Intel’s ForSpec.
This work was recognized as one of the top accomplishments of the IBM Almaden Research Center in 1987, won an IBM Outstanding Innovation Award in 1989, and the Gödel Prize (with P. Wolper) in 2000. PSL 1.1, an industrial-standard property-specification language in whose design I was involved, won a DesignVision Award from the International Engineering Consortium (IEC) in 2005, and has been established as IEEE Std 1850-2005.
Finite-Model Theory: Model theory is a study of the logical properties of mathematical structures such as graphs and groups; finite-model theory focuses on finite structures. Finite-model theory is highly relevant to computer science, because of the intimate connection it has to several areas such as complexity theory, database theory and logic programming. For example, some of the most fundamental questions in complexity theory are equivalent to questions in finite-model theory. This is illustrated by a result of mine (obtained independently also by Immerman) that characterized the complexity class of polynomial time is terms of first-order logic enriched with the fixpoint operator.
Of special interest is the study of asymptotic probabilities for properties of finite structures. The asymptotic probability of a property on the collection of all finite structures is the limit, as n gets arbitrarily large, of the fraction of structures with n elements satisfying the property, provided the limit exists. This probability can be viewed as the likelihood that an “average” graph satisfies the property. Kolaitis I investigated the asymptotic probability of certain classes of NP properties. These classes are expressible in fragments of existential second-order logic in which we restrict the patterns of first-order quantifiers. We proved that several such classes have a 0-1 law, i.e., the asymptotic probabilities of properties in these classes is always either 0 or 1.
This work was recognized as of the top accomplishments of the IBM Almaden Research Center in 1990, and won an IBM Outstanding Innovation Award in 1992.
Any further pages in alphabetic order of their title as created by you.
#
Just click at "Create new page", then type a short title and click OK, then add information on the empty page presented to you (including maybe a picture from your harddisk or a pdf-file by using the "Upload" Button) and finally click at "Save".
...no Data available yet!
