Exploiting Local Symmetries to Ameliorate State Explosion in Model Checking

State-space explosion is the primary obstacle to the scalability of model checking. For programs structured as a process network, the symmetries of the network may be utilized to ameliorate state explosion. In the best situation of full symmetry, it is possible to achieve an exponential reduction in the state space. However, commonly used topologies, such as the ring, mesh, torus and hypercube, have little global symmetry. On the other hand, these networks have a regular structure that exhibits many local symmetries. Motivated by this observation, we develop reductions based on the local symmetries of a network. We introduce two key concepts: partial symmetry action, structured as a groupoid; and the notion of symmetry under abstraction. Application of these concepts helps uncover new symmetries; we show that it is possible to obtain exponential reductions for the state spaces of complex protocols, whereas existing methods provide only a polynomial reduction.