Given a program P , one can construct a Kripke structure \(\mathcal{M}\) . Model checking verifies that P satisfies a behavioral property given by a temporal logic formula \(\varphi\) by checking that \(\mathcal{M}\) models \(\varphi\) . However, \(\mathcal{M}\) can be exponentially large in P . The action of a symmetry group G on \(\mathcal{M}\) and \(\varphi\) can produce a smaller structure \(\overline{\mathcal{M}}\) . When \(\mathcal{M}\) does not satisfy \(\varphi\) , one can look for a substructure that satisfies \(\varphi\) . We call this substructure repair . We show that repairs of \(\overline{\mathcal{M}}\) lift to repairs of \(\mathcal{M}\) , i.e., we can repair a concurrent program by repairing the smaller structure \(\overline{\mathcal{M}}\) and symmetrizing the resulting program. The substructures of \(\overline{\mathcal{M}}\) map to substructures of \(\mathcal{M}\) preserved by G . We present relative completeness results, which give conditions under which the existence of a repair of \(\mathcal{M}\) implies the existence of a repair of \(\overline{\mathcal{M}}\) . In cases where there is no repair of a Kripke structure \(\mathcal{M}\) w.r.t. a formula, we show that there are instances where it is possible to “unwind” \(\mathcal{M}\) to generate a structure \(\mathcal{M^{\prime}}\) that is strongly bisimilar to \(\mathcal{M}\) and for which a repair exists. This leads to a natural semantic notion, repairability , which is not preserved by strong bisimulation. We illustrate the combined use of symmetry reduction and unwinding to effect a repair. Finally, we provide closed-form results for the reductions in number of states in the Kripke structure that can be achieved by symmetry reduction.

Abstract Given a textual representation of a finite-state concurrent program $$P$$ P , one can construct the corresponding Kripke structure $$\mathcal {M}$$ M . However, the size of $$\mathcal {M}$$ M can be exponentially larger than the textual size of $$P$$ P . This state explosion can make model checking properties of $$P$$ P via $$\mathcal {M}$$ M expensive or even infeasible. The action of a symmetry group $$G$$ G on $$\mathcal {M}$$ M can be used to produce a smaller Kripke structure $$\overline{\mathcal {M}}$$ M ¯ . Various authors have exploited the direct correspondence between $$\mathcal {M}$$ M and $$\overline{\mathcal {M}}$$ M ¯ to perform model checking. When the structure $$\mathcal {M}$$ M does not satisfy a formula, one can look for a substructure that will satisfy the formula. We call this substructure-repair : identifying a substructure $$\mathcal {N}$$ N of $$\mathcal {M}$$ M that satisfies a given temporal logic formula. In this paper we extend previous work by showing that repairs of $$\overline{\mathcal {M}}$$ M ¯ lift to repairs of $$\mathcal {M}$$ M . In other words, we can repair a computer program $$P$$ P , which exhibits a high degree of symmetry, by repairing the smaller Kripke structure $$\overline{\mathcal {M}}$$ M ¯ and then symmetrizing the corresponding program. To do this we arrange the substructures of $$\mathcal {M}$$ M and $$\overline{\mathcal {M}}$$