Symmetry Reduction for the Local Mu-Calculus

TL;DR

This paper demonstrates that local properties in network models can be verified efficiently using neighborhood symmetries, significantly reducing computational costs even in networks with limited global symmetry.

Contribution

It generalizes invariance results to all local mu-calculus properties, enabling local verification that approximates or equals global verification under certain conditions.

Findings

Neighborhood symmetries preserve local mu-calculus properties.

Verification cost is exponentially reduced using representatives.

Applicable to network families from building blocks.

Abstract

Model checking large networks of processes is challenging due to state explosion. In many cases, individual processes are isomorphic, but there is insufficient global symmetry to simplify model checking. This work considers the verification of local properties, those defined over the neighborhood of a process. Considerably generalizing earlier results on invariance, it is shown that all local mu-calculus properties, including safety and liveness properties, are preserved by neighborhood symmetries. Hence, it suffices to check them locally over a set of representative process neighborhoods. In general, local verification approximates verification over the global state space; however, if process interactions are outward-facing, the relationship is shown to be exact. For many network topologies, even those with little global symmetry, analysis with representatives provides a significant, even exponential, reduction in the cost of verification. Moreover, it is shown that for network families generated from building-block patterns, neighborhood symmetries are easily determined, and verification over the entire family reduces to verification over a finite set of representative process neighborhoods.