Computer Science – Software Engineering
Scientific paper
2005-01-22
Computer Science
Software Engineering
Scientific paper
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.
No associations
LandOfFree
Under-approximation of the Greatest Fixpoint in Real-Time System Verification does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Under-approximation of the Greatest Fixpoint in Real-Time System Verification, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Under-approximation of the Greatest Fixpoint in Real-Time System Verification will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-279623