Under-approximation of the Greatest Fixpoint in Real-Time System Verification

Abstract

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\eta_1\), \(\exists\pfrr\pevt\eta_1\), and \(\exists\pevt\pfrr\eta_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\eta_1\), \(\exists\pfrr\pevt\eta_1\), and \(\exists\pevt\pfrr\eta_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.