Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Model checking with strong fairness
Kesten Y., Pnueli A., Raviv L., Shahar E. Formal Methods in System Design28 (1):57-84,2006.Type:Article
Date Reviewed: Nov 23 2006

Classical model checking methods for temporal logic formulas suffer from the problem of unsatisfactory treatment of fairness—only a weak form of fairness, “justice,” is directly addressed. “Compassion,” a strong form of fairness, involves the use of multiple frameworks (like mu calculus or linear temporal logic (LTL)) while using model checking computational tree logic (CTL) formulas. Further enumerative (nonsymbolic) model checking of LTL formulas is also used in classical analysis. This paper addresses the shortcomings of classical approaches using a coherent framework for symbolic model checking of temporal logic formulas, taking into account full fairness directly at the algorithmic level, without resorting to other logics.

The core of the basic framework is a symbolic feasible state computation algorithm. This algorithm, given a fair transition system, computes the set of all feasible states, the states that are reachable from initial states via a fair path. Model checking of LTL formulas, as usual, is reduced to an emptiness check of the synchronous product of the given transition system and the transition system corresponding to the LTL formula. Model checking of general CTL formulas is based on the Emerson-Lei recursive algorithm, which invokes the feasible state computation algorithm.

The paper concludes with an interesting experimental study comparing the proposed framework with the existing approaches to fairness. This experimentation shows that the proposed framework is preferable to the existing methods.

The paper is well written, conveying the basic problem and the solution, and putting the results of the paper into context. It is a useful reference for researchers in the area of model checking. Some background in formal modeling, verification, and fairness is assumed. Readers without this background would find the paper difficult to understand. The proofs of the results are sketchy and informal. Surprisingly, the complexities of the algorithms are not discussed in the paper.

Reviewer:  S. Ramesh Review #: CR133621 (0711-1120)
Bookmark and Share
  Featured Reviewer  
 
Model Checking (D.2.4 ... )
 
 
Analysis Of Algorithms (I.1.2 ... )
 
 
Automatic Analysis Of Algorithms (I.2.2 ... )
 
 
Evaluation Strategies (I.1.3 ... )
 
 
Symbolic Execution (D.2.5 ... )
 
 
Temporal Logic (F.4.1 ... )
 
  more  
Would you recommend this review?
yes
no
Other reviews under "Model Checking": Date
Systems and software verification: model-checking techniques and tools
B ., Bidoit M., Finkel A., Laroussinie F., Petit A., Petrucci L., Schnoebelen P., McKenzie P., Springer-Verlag New York, Inc., New York, NY, 1999.  190, Type: Book (9783540415237)
Sep 30 2002
Module checking
Kupferman O., Vardi M., Wolper P. Information and Computation 164(2): 322-344, 2001. Type: Article
Mar 1 2002
SMC: a symmetry-based model checker for verification of safety and liveness properties
Sistla A., Gyuris V., Emerson E. ACM Transactions on Software Engineering and Methodology 9(2): 133-166, 2000. Type: Article
Sep 1 2000
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy