一句话：提出 LTL 反例的合取式因果定义与计算算法，改进模型检测反例诊断。
模型检测可判断系统是否满足规约，但 LTL 性质违反的反例诊断仍困难。现有因果推理方法在表达力、复杂依赖识别或计算可行性上受限。本文重新定义 LTL 反例中的 cause，使其支持合取原因（conjunctive causes），并给出计算这些原因的新算法。作者在工业规约基准上与基线因果计算算法比较；在所有比较中，新算法要么包含基线原因、要么识别更强原因，要么以可解释方式与基线不同，表明其能增强反例分析。
Model checking and verification play a crucial role in ensuring the correctness of software systems by systematically analyzing whether a system satisfies desired specifications. Diagnosing property violations in LTL counterexamples is essential for debugging and refining software, helping developers identify faults and ensure requirement compliance. Several approaches have considered the use of causal reasoning to aid in the identification and explanation of counterexamples. However, these methods are often limited in their expressivity, ability to recognize complex dependencies in system behaviors, or computational feasibility. This paper proposes a revised definition of causes for LTL violations in counterexamples, allowing for the identification of conjunctive causes. Additionally, we introduce a novel algorithm for computing such causes and compare it against a baseline causal computation algorithm using a benchmark of industrial specifications. In all comparisons, our algorithm either subsumes baseline causes, identifies stronger causes, or diverges from the baseline in explainable ways, demonstrating its effectiveness in enhancing counterexample analysis.