Knowledge-based programs

Reasoning about activities in a distributed system at the level of knowledge allows us to abstract away from many irrelevant details. We introduce two notions to facilitate designing and reasoning about systems in terms of knowledge. The first is knowledge-based programs, which improve upon Halpern and Fagin's definition of knowledge-based protocols. Knowledge-based programs are syntactic objects: programs with tests for knowledge. The second notion is contexts, which capture the setting in which a program is executed. In a given context, a standard program (one without tests for knowledge) is represented by (i.e., corresponds in a precise sense to) a unique system. A knowledge-based program, on the other hand, may be represented by no system, one system, or many systems. We provide a condition that is sufficient to guarantee that a knowledge-based program is represented by a unique system, and covers many of the knowledge-based programs considered in the literature. We also characterize the complexity of determining whether a given knowledge-based program has a unique representation, or any representation at all, in a finite-state context.