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.