OLENDER@SRI-AI.ARPA.UUCP (05/13/86)
DATE: May 14, 1986
TIME: 4:15pm
TITLE: "Knowledge, Communication, and Time"
SPEAKER: Van Nguyen
LOCATION: SRI International
Ravenswood Avenue
Building E
CONFERENCE ROOM: EJ228
KNOWLEDGE, COMMUNICATION, AND TIME
Van Nguyen
IBM Thomas J. Watson Research Center
(Joint work with Kenneth J. Perry)
The role that knowledge plays in distributed systems has come under
much study recently. In this talk, we re-examine the commonly
accepted definition of knowledge and examine how appropriate it is for
distributed computing. Motivated by the draw-backs thus exposed, we
propose an alternative definition that we believe to be better suited
to the task. This definition handles multiple knowers and makes
explicit the connection between knowledge, communication, and time.
It also emphasizes the fact that knowledge is a function of one's
initial knowledge, communication history and deductive abilities. The
need for assuming perfect reasoning is mitigated.
Having formalized these links, we then present the first proof
system for programs that incorporates both knowledge and time. The
proof system is compositional, sound and relatively complete, and is
an extension of the Nguyen-Demers-Gries-Owicki temporal proof system
for processes. Suprisingly, it does not require proofs of
non-interference (as first defined by Owicki-Gries).
-------