1 prod iterates through all product states  The inner loop of       prod iterates through all  F
atoms Note that and FSA transition function tables built for prod does at most   lookups for each table entry By comparison  our incremental algorithm     prod for generating the product FSA has time complexity FSA for Invariance property reverification or AT reverification  respectively  This is because the total number of revised product states is  Π n = 1
*
and 1. I
only one atom is considered  because we assume  change changes the next state for a single atom   adapt    The time complexity of     prod-N1 is the same as that of prod Next consider the worst case time complexity of total  re verification after the product has been formed  It is for worst case every product state is accessible and therefore every entry in the product FSA
transition function table is visited Assuming       is the number of   bad"   in the Buchi sense states in the product FSA  then the worst case time complexity of i This is because  in the worst case  every entry in the product n" FSA transition function table is visited once on the depth first search and  for each bad state again on the nested depth first search Unfortunately the worst case time complexity I -NI and AT-NI are the same as that of AT and AT respectively This is because in the worst case every product state is still accessible The restriction to transition only on  adapt at first does not reduce the  big O" complexity Finally  we consider the worst case complexity of    gen-r and    gen-r  First  we define for any Boolean expression and L
For Invariance properties of the form □              equals      since we test for each atom rather than because we expect in general   Then w het her gen - I
requires time requires constant time   Assuming bizarre circumstances   and since                          gen-i saves time over I
gen - R
to determine whether requires time and then to
*
13 Clearly determine whether and and and
≤ 
of gen Therefore assuming
* 
w hich again  should be true except in bizarre circumstances   the worst case time complexity of gn-R is lower than that of AT

## 6.5   Empirical  Time  Complexity  Comparisons

Worst case time complexity is not always a useful measure  Therefore we supplement the worst case analyses with empirical results on cpu time  Our primary objective in these experiments is to compare the incremental algorithms with total reverification  as well as with each other  for the context of evolving behaviorally correct FSAs  The time required