Model and Program Repair via Group Actions

Given a textual representation of a finite-state concurrent program P, one can construct the corresponding Kripke structure M. However, the size of M can be exponentially larger than the textual size of P. This state explosion can make model checking properties of P via M expensive or even infeasible. The action of a symmetry group G on M can be used to produce a smaller Kripke structure M¯. Various authors have exploited the direct correspondence between M and M¯ to perform model checking. When the structure 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 N of M that satisfies a given temporal logic formula. In this paper we extend previous work by showing that repairs of M¯ lift to repairs of M. In other words, we can repair a computer program P, which exhibits a high degree of symmetry, by repairing the smaller Kripke structure M¯ and then symmetrizing the corresponding program. To do this we arrange the substructures of M and M¯ into substructure lattices that are ordered by substructure inclusion. We show that the substructures of M preserved by G form a (sub)lattice that maps to the substructure lattice of M¯. When restricted to the lattice of substructures of M that are “maximal” with the action of G on M, the above map is a lattice isomorphism. These results enable us to repair M¯ and then to lift the repair to M. In cases where a program has a high degree of symmetry, such as in many concurrent programs, we can repair the program by repairing the small Kripke structure M¯.