Model Repair via Symmetry

TL;DR

This paper extends symmetry-based model checking to model repair, allowing the identification and repair of substructures satisfying temporal logic formulas efficiently by leveraging symmetry to avoid state explosion.

Contribution

It introduces a method to repair models via symmetry, establishing a lattice and Galois connection framework to lift repairs from quotient structures to original models.

Findings

Enables repair of symmetric models by working on smaller quotient structures.

Establishes a lattice and Galois connection framework for substructure analysis.

Facilitates program repair while avoiding state explosion.

Abstract

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.