一句话：提出性质精化关系，判定CTL性质间的语义蕴含，识别冗余性质，最高减少70%规范并加速验证30倍。
形式验证依赖以CTL形式化的规范来描述系统行为，但在迭代设计周期中，规范套件不断增长与演化，积累了大量重叠且语义依赖的性质，带来规范债务，增加工程与验证成本。本文提出通过性质精化（property refinement）来应对这一问题：精化关系刻画性质之间的语义关联，判定某个性质是否已被另一性质所保证，从而为需求管理提供工程洞见，并帮助识别冗余性质。评估表明，该方法可将规范规模最多缩减70%，验证速度最多提升30倍，展示了在优化验证工作流、引导工程师聚焦真正必要性质方面的实际潜力。
Formal verification relies on specifications formalized in CTL to express desired system behaviors. In practice, specification suites grow and evolve during iterative design cycles, accumulating overlapping and semantically dependent properties that increase engineering and verification cost. We propose to address this specification debt via property refinement, which captures semantic relationships between properties, identifying when one property is already guaranteed by another. This provides engineering insights into these semantic relationships, easing requirements management and the identification of redundant properties. Our evaluation shows reductions of up to 70% and speedups of up to 30 times, showcasing the practical potential in optimising verification workflows and guiding engineers towards identifying what is really needed.