Local Symmetry and Compositional Verification
01 January 2012
We explore the connections between compositional reasoning for networks of processes and local symmetry. Many networks, such as rings, have a small global symmetry group, which limits the symmetry reduction in standard model checking. On the other hand, we show that for compositional reasoning, it suffices to look for local symmetries in the network (i.e., similarity based on neighborhood) and that significant reductions are possible as a result. Technically, local symmetries are represented by a symmetry groupoid a generalization of the symmetry group which induces a reduced quotient network. In the paper, we formulate a simple local reasoning principle for general networks, define the symmetry groupoid and the quotient construction, and give examples of reduction using local symmetries.
