Knowledge-based Verification and Construction of Distributed and Constrained Systems

Deriving distributed implementations from global specifications has been extensively studied for various application domains, and under various assumptions and constraints.
We explore here the problem from the knowledge perspective: a process can decide to execute a local action when it has the knowledge to do so. We discuss typical knowledge atoms, useful for expressing local enabling conditions with respect to different notions of correctness, as well as different means for obtaining knowledge and for representing it locally in an efficient manner.
Our goal is to use such a knowledge-based representation of the distribution problem for either deriving distributed implementations automatically from global specifications on which some constraint is enforced – a difficult problem – or for improving the efficiency of existing protocols by exploiting local knowledge. We also argue that such a knowledge-based presentation helps achieving the necessary correctness proofs.