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

TL;DR

This paper introduces a new framework and algorithms for efficiently under-approximating the greatest fixpoint in real-time system verification, improving performance in model-checking tasks involving inevitability properties.

Contribution

The paper presents a novel NZF predicate and a unified fixpoint evaluation framework enabling successful successive under-approximation in real-time system model-checking.

Findings

Significantly improved verification performance on benchmarks.

Effective zone search techniques for faster under-approximation.

Validated correctness of the new fixpoint characterization.

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.