Modal logics of knowledge have been proposed as a formalism for the study of information flow in distributed and multi-agent systems. In particular, the notion of knowledge-based programs, in which agents condition their actions on formulas expressing what they know, has been argued to provide a level of abstraction that leads to simple correctness proofs, an ability to capture commonalities between protocols that operate under different environmental assumptions, and the ability to specify that information accesible to the agents is used in an optimal way.

Knowledge-based programs cannot be directly executed, however, but are better understood as specifications that can be said to be satisfied by concrete implementations. This leads to the problems of verification and synthesis for knowledge-based programs. The talk will survey work on the algorithmic solution of these problems, their implementation in the model checker MCK, which uses symbolic techniques (BDD's) to model check specifications in the logic of knwoeldge and time. An application of this system to the analysis of cache coherency will be discussed which has automatically identified a non-optimal behavior of the Synapse protocol.