Group routing without group routing tables

We present a group routing protocol for a network of processes. The task of the protocol is to route data messages to each member of a process group. To this end, a tree of processes is constructed in the network, ensuring each group member is included in the tree. To build this tree, the group routing protocol relies upon the unicast routing tables of each process. Thus, group routing is a composition of a unicast routing protocol, whose detailed behavior is unknown but its basic properties are given, and a protocol that builds a group tree based upon the unicast routing tables. The design of the group routing protocol is presented in three steps. First, a basic group routing protocol is presented and proven correct. Then, the protocol is refined twice, strengthening its properties with each refinement. The final protocol has the property of adapting the group tree to changes in the unicast routing tables without compromising the integrity of the group tree, even in the presence of unicast routing loops