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

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.

Abstract licence: CC0

A person counts once a day per paper. We keep no cookie and no address: a reader is a hash that changes every day. Any month under five reads shows no number.