Refining knowledge oriented actions to layered implementations

Abstract

Knowledge based logics and knowledge based protocols allow to give generic specifications of network protocols and distributed algorithms in general. The question of how to transform a knowledge based program into a standard one is still largely unsolved however. In this paper we propose two knowledge oriented actions, COMBINE and NOTIFY, that allow for the transformational development of standard protocols from knowledge based specifications and protocols. These actions combine distributed knowledge and spread knowledge respectively. Using NOTIFY and COMBINE one can give generic implementations and specifications of a large class of network protocols, and can derive implementations tailored to specific architectures in a straightforward, transformational way. The method to derive implementations relies on the notions of layering and communication closedness. It is applicable to a large class of protocols that have an underlying sequential structure. We illustrate the approach with the derivation of an algorithm to compute distances in networks and some smaller examples, aiming at implementations using asynchronous message passing. However, the method can be used in other settings as well.