  The symmetry of a Kripke structure $\mathcal{M}$ has been exploited to
replace a model check of $\mathcal{M}$ by a model check of the potentially
smaller structure $\mathcal{N}$ obtained as the quotient of $\mathcal{M}$ by
its symmetry group $G$. We extend previous work to model repair: identify a
substructure that satisfies a given temporal logic formula. We show that the
substructures of $\mathcal{M}$ that are preserved by $G$ form a lattice that
maps to the substructure lattice of $\mathcal{N}$. We also show the existence
of a monotone Galois connection between the lattice of substructures of
$\mathcal{N}$ and the lattice of substructures of $\mathcal{M}$ that are
"maximal" w.r.t. an appropriately defined group action of $G$ on $\mathcal{M}$.
These results enable us to repair $\mathcal{N}$ and then to lift the repair to
$\mathcal{M}$. We can thus repair symmetric finite-state concurrent programs by
repairing the corresponding $\mathcal{N}$, thereby effecting program repair
while avoiding state-explosion.
