Incremental CTL model checker for fair states

CTL (Computation Tree Logic) model checking is a formal method for design v erification that checks whether the behavior of the verified system is cont ained in that of the requirements specification. If this check doesn't pass , the CTL model checker generates a subset of fair states which belongs to the system but not to the specification. In this letter, we present an incr emental method which successively modifies the latest verification result e ach time the design is modified. Our incremental algorithm allows the desig ner to make changes in terms of addition or subtraction of fair CTL formula s, or fairness constraints on acceptable behavior from the problem statemen t. Then, these changes are adopted to update the set of fair states compute d earlier. Our incremental algorithm is shown to be better than the current non-incremental techniques for CTL model checking. Furthermore, a conclusi on supported by the experimental results is presented herein.