实时系统验证中最大不动点的欠近似

在 TCTL 公式中高效连续欠近似最大不动点的技术可用于必然属性的快速反驳与空性检查。我们首先给出用于欠近似与过近似模型检验的集成算法框架。我们设计了具有最大不动点形式的 NZF（Non-Zeno Fairness，非齐诺公平性）谓词，作为如 $\exists\pfrr\eta_1$、$\exists\pfrr\pevt\eta_1$ 与 $\exists\pevt\pfrr\eta_1$ 等公式求值的统一框架。随后我们证明了基于区域搜索与最小不动点求值的 NZF 谓词刻画新形式的正确性。该新形式进而导出了具有连续欠近似能力的、针对 $\exists\pfrr\eta_1$、$\exists\pfrr\pevt\eta_1$ 与 $\exists\pevt\pfrr\eta_1$ 的求值算法设计。接着我们给出高效搜索区域及加速这三式欠近似求值的技术。实验表明，相较精确模型检验，这些技术对若干基准的验证性能有显著提升。