AI 中文总结
针对混合迹网的安全验证，提出可达性松弛方法，高效识别不变量以缩减状态空间，实验证明在更多实例中证明不可达且生成更多不变量、速度更快。
AI 中文摘要
故障和错误检测对于确保安全关键系统的正确性至关重要。安全验证通常涉及对不良系统状态的可达性分析，而在复杂系统中，由于状态空间庞大，穷举状态检查可能难以处理。我们针对混合迹网（一种用于分析并发事件系统的有用数学模型）提出了一种可达性松弛方法，以高效验证系统安全性。我们进一步利用该松弛方法有效识别不变量（在所有可达状态下均成立的表达式），从而缩减状态空间以实现高效验证。实验结果表明，在测试问题中，我们的方法在1.5倍更多的实例中证明了不安全状态不可达，生成的不变量数量是基线的2.5倍，且生成时间比基线快最多两个数量级。
英文摘要
Fault and error detection is crucial for ensuring the correctness of safety-critical systems. Safety verification often addresses reachability of bad system states, where exhaustive state inspection may be intractable due to the large state spaces of complex systems. We propose a reachability relaxation for hybrid trace nets, a useful mathematical model for analyzing concurrent event systems, to efficiently verify system safety. We further use our relaxation to effectively identify invariants, expressions that hold in all reachable states, allowing state-space reduction for efficient verification. Empirically, our approach proves unsafe states unreachable in 1.5x more instances, generates 2.5x more invariants with up to 2 orders of magnitude faster generation times than the baselines in the tested problems.
Comments8 pages. Submitted to The 2027 American Control Conference (ACC)
