The Computer Science Colloquium

Ron van der Meyden
(Computer Science and Engineering University of New South Wales, Sydney, Australia)

"Knowledge-Based Programs: a methodology using model checking and refinement"

Viewing agents that have to operate subject to uncertainty about their environment as having "states of knowledge" provides a highly intuitive level of abstraction, that replaces a focus on the local states of agents by consideration of the information that these states encode. The usefulness of this abstraction for analytic purposes has led to proposals for _knowledge-based programs_, in which agents' actions have preconditions expressed in modal logics of knowledge. It has been argued that knowledge-based programs can provide uniform descriptions of apparently unrelated distributed systems protocols, operating with respect to different assumptions concerning the communications substrate, and lead to protocols that are optimal in their use of information.

These benefits come at a cost, however: knowledge-based programs cannot be directly executed, but are more like specifications that must be _implemented_ by translating the tests for knowledge into concrete computations based on the agents' local states. Since the agents' knowledge depends on their behaviour, which in turn depends on their knowledge, this is a nontrivial problem, involving the solution of a fixpoint equation.

The talk will survey some recent work that aims to overcome some of the inherent difficulties in knowledge-based programming by means of a generalised notion of knowledge-based programs, calculi for the refinement of knowledge level specifications to implementations, and the development of tool support for the automated analysis of implementations.

The Colloquium is supported by generous contributions from the Bloomberg, Information Builders, Inc., and Netlogic, Inc.