In this work, we consider distributed protocols that operate on arbitrary networks. The analysis of such protocols is challenging, as an arbitrarily chosen network may have limited global symmetry. We describe a methodology that uncovers significant local symmetries by appropriately abstracting node neighborhoods in a network. The local symmetries give rise to uniform compositional proofs of correctness. As an illustration of these ideas, we show how to obtain a uniform compositional invariance proof for a Dining Philosophers protocol operating on a fixed-size, arbitrary network. An interesting and somewhat unexpected consequence is that this proof generalizes easily to a parametric proof, which holds on any network regardless of size or structure.
展开▼
