PRL Seminars

Abstract

Knowledge-based protocols, where an agent's actions depend not just on his local state, but also on his knowledge (proposed by Halpern and Fagin in 1989), have been successfully used in distributed settings and in proving uniform correctness proofs for families of protocols. However, automatic synthesis of knowledge-based protocols is still an open problem. It is important to understand what happens when we add knowledge-based specifications to a powerful system that allows automatic synthesis of protocols, as Nuprl.

We choose to add knowledge-based specifications on top of the logic of events as it is straightforward to model the consistent cuts semantics for epistemic logic using event systems. Our formalization allows us to emulate the results on knowledge-based protocols for the bit sequence transmission presented by Halpern and Zuck in A little knowledge goes a long way (1992). This enables us to comment on some aspects of extracting protocols from knowledge specifications.