论文标题
通过对称性修复模型
Model Repair via Symmetry
论文作者
论文摘要
通过使用模型检查$ \ Mathcal {N} $的模型检查，将Kripke结构的对称性$ \ MATHCAL {M} $替换为$ \ Mathcal {M} $的模型检查，以$ \ MATHCAL {M} $的对中的{M} $的对中的{M} $的对中的{M} $的对中的{N} $。我们将以前的工作扩展到模型维修：确定满足给定时间逻辑公式的子结构。我们表明，由$ g $保留的$ \ Mathcal {M} $的子结构形成一个晶格，该晶格映射到$ \ Mathcal {n} $的子结构晶格。我们还展示了$ \ Mathcal {n} $的子结构的晶格与$ \ Mathcal {M {m} $的子结构的晶格之间的单调galois连接存在。 $ \ MATHCAL {M} $上适当定义的$ G $的组动作。这些结果使我们能够维修$ \ Mathcal {n} $，然后将维修提高到$ \ Mathcal {M} $。因此，我们可以通过修复相应的$ \ Mathcal {n} $来修复对称的有限状态并发程序，从而在避免状态探索的同时效力程序维修。
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.
