Model and Program Repair via Group Actions and Structure Unwinding

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.