实时的系统验证中最大不动点的欠逼近
Under-approximation of the Greatest Fixpoint in Real-Time System Verification
摘要：
TCTL公式中最大不动点的有效逐次欠逼近技术可用于快速反驳必然性和真空性检验。我们首先给出了一个综合的算法框架下和过近似模型检查。我们设计了{ \em NZF（Non-Zeno Fairness）谓词}，具有最大不动点公式，作为评估公式（如$\exists\pfrrη_1$、$\exists\pfrr\pevtη_1$和$\exists\pevt\pfrrη_1$）的统一框架。然后，我们证明了一个新的配方的NZF谓词的区域搜索和最少的不动点评价的基础上表征的正确性。新的配方，然后导致一个评估算法的设计，与连续下近似的能力，为$\exists\pfrrη_1$，$\exists\pfrr\pevtη_1$，和$\exists\pevt\pfrrη_1$。然后，我们提出的技术，有效地搜索的区域，并加快这三个公式的近似评估。我们的实验表明，该技术已显着提高了对几个基准的验证性能超过精确的模型检查。
英文摘要：
Techniques for the efficient successive under-approximation of the greatest fixpoint in TCTL formulas can be useful in fast refutation of inevitability properties and vacuity checking. We first give an integrated algorithmic framework for both under and over-approximate model-checking. We design the {\em NZF (Non-Zeno Fairness) predicate}, with a greatest fixpoint formulation, as a unified framework for the evaluation of formulas like $\exists\pfrrη_1$, $\exists\pfrr\pevtη_1$, and $\exists\pevt\pfrrη_1$. We then prove the correctness of a new formulation for the characterization of the NZF predicate based on zone search and the least fixpoint evaluation. The new formulation then leads to the design of an evaluation algorithm, with the capability of successive under-approximation, for $\exists\pfrrη_1$, $\exists\pfrr\pevtη_1$, and $\exists\pevt\pfrrη_1$. We then present techniques to efficiently search for the zones and to speed up the under-approximate evaluation of those three formulas. Our experiments show that the techniques have significantly enhanced the verification performance against several benchmarks over exact model-checking.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
