Implementing knowledge-based programs

Reasoning about multi-agents systems at the knowledge level allows us to abstract away from many concrete details of the systems we are considering. Fagin et al. introduced two notions to facilitate designing and reasoning about systems in terms of knowledge. The first notion is that of knowledge-based programs. Knowledge-based programs are defined as syntactic objects: programs with tests for knowledge. The second notion is that of contexts, which capture the setting in which a program is to be executed. In a given context, a standard program (one without tests for knowledge) is always implementable. A knowledge-based program, on the other hand, might not be implementable. We provide a condition which is necessary and sufficient to guarantee that a given knowledge-based program is implemented by a given protocol, and we completely characterize the complexity of determining whether a given knowledge-based program is implemented by a given protocol in a given finite-state context. In particular, we identify an important special case where this problem is tractable.