Using Computation Tree Logic we can reason about various properties of a computation via its Kripke structure. A Kripke structure is a model of computation, similar to an automata, that captures the possible states and transitions of a computation. When a Kripke structure fails to satisfy a given property, we may ask if there is a substructure that does satisfy this property; such a substructure is called a repair of the original structure. In general, model checking or repairing a Kripke structure is difficult due to the size of a Kripke structure in relation to its underlying program. In this talk we demonstrate how group actions can be used to construct a quotient structure of a given Kripke structure that is bisimilar with respect to a given formula. This bisimilarity establishes a Galois correspondence between repairs of the quotient structure and certain repairs of the original structure. Moreover, it is possible to construct the quotient structure directly from a textual program, and repair the textual program via the repair of the quotient. This avoids the need to construct the larger structure.