Constructing finite state implementations of knowledge-based programs with perfect recall

Knowledge-based programs have been proposed as an abstract formalism for the design of multi-agent protocols, based on the idea that an agent's actions are a function of its state of knowledge. The key questions in this approach concern the relationship between knowledge-based programs and their concrete implementations, in which the actions are a function of the agents' local states. In previous work we have shown that with respect to a perfect recall semantics for knowledge, finite state implementations of knowledge-based programs do not always exist. Indeed, determining the existence of such an implementation is undecidable. However, we also identified a sufficient condition under which the existence of a finite state implementation is guaranteed, although this sufficient condition is also undecidable. We show in this paper that there nevertheless exists an approach to the optimization of implementations that results in a finite state implementation just when the sufficient condition holds. These results contribute towards a theory of automated synthesis of multi-agent protocols from knowledge-based specifications.