!!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".\\
[{CategoryIndexPlugin category='User/Vardi_Moshe/Highlight'}]