 Procedure check-invariance-property if v 1 was not previously visited, then output "Verification succeeds." else if ( z |=   p ) then output "Verification succeeds."
else output "Avoid this instance of ogen " ; endif endif end procedure

## Figure Gen - 1 Reverification Algorithm

is localized ie  that it is  gen with     lagent Or multplans where gen might become  ada   An important advantage of these algorithms is that they never require forming a product FSA  not even           regardless of whether the property is type Response  The algorithms gain efficiency by being       tailored to a specific property to a specific learning operator  The objective in developing these algorithms was type maximal efficiency and therefore they sacrifice completeness and or the ability to find all errors These two incremental algorithms are tailored for reverification after operator  gen Assume that property holds for prior to learning ie Now we generalize the to form  ' via  gen    K   1   3 transition condition where We want to verify that '
One additional definition is needed before presenting our algorithms  We previously defined what it means for a c state formula   to be true at a c state  but to simplify the algorithms we also define what it means for a c state formula to be true of a transition condition A c state formula is defined to be true of a transition condition i e if and only if which can be implemented by testing whether for every atom Let us begin with the algorithm    gen-1  which consists of two very simple tests tailored for  gen and Invariance properties  shown in Figure      Recall that    κ    ι   з gen - 1  which tests           " localizes reverification to a and gen K 1 3 restricted portion of the FSA  For efficiency is implemented as a test for rather than           because   is typically expected to be more succinct than Assume the Invariance property is st is fies Invariance property so for each x is true of every atom in x This implies This statement is based on our assumption that 1 is accessible from an initial state If not reverification is not needed  The generalization will not violate     Therefore  the algorithm begins by testing whether 1 was visited on previous verification If not the output is success " Note that gen does not alter the accessibility of 1 gen - 1 is sound and complete for Invariance properties  Generalization of    κ   1   3 is application of gen to form ' This operator gen preserves Invariance property     if and only if           which is true if and only if The reason for this is that we know   satisfies    from our original verification  and therefore      is true for all atoms in all strings in        The only possible new atoms in      '  but not in are then is true for all atoms in in If