Aspects Of Knowledge And Belief-Based Programming

Abstract

It has long been recognized that many distributed problems can be analyzed in terms of how agents act based on what they know about the system they are in. To make this intuition formal, Fagin, Halpern, Moses, and Vardi [25, 26] proposed a theory of programs for multi-agent systems in which preconditions of actions are formulas in a logic of knowledge. Knowledge-based programs have been successfully applied to a number of fundamental problems. This dissertation aims at further investigating the role of knowledge-based programs in the study of distributed systems. We focus ?rst on a general problem in distributed settings: given a function f whose value depends on the whole network N , the goal is for every agent to eventually compute the value f (N ). We call this problem global function computation. We give a necessary and suf?cient condition for the problem to be solvable and provide a knowledge-based program that solves the global function computation problem whenever possible. The program guarantees a certain level of optimality by having agents send messages only when they believe it is necessary to do so, and allows for systems in which agents are anonymous. Second, we consider the synthesis of knowledge-based programs. In general, to produce a program guaranteed to satisfy a given speci?cation, one can try to synthesize it from a formal proof that a computation satisfying that speci?cation exists. We build on a technique proposed by Bickford and Constable [11, 12] for extracting message automata from speci?cations of multi-agent systems to show how knowledge-based message automata can be synthesized using a proof development system such as Nuprl [19]. Third, we consider the problem of ensuring secrecy in a multi-agent system by disallowing unwanted ?ows of information. We discuss knowledge-based formulations of information-?ow properties, with a focus on the basic security predicates in the Modular Assembly Kit proposed by Mantel [62].