and the property is true prior to learning ie  for     then it is possible that a response is required  In this situation  i e the only way to be sure we are safe '
is if to the newly added condition also has the response i e If not  then there could be new strings in For example suppose a b c and d are atoms and the transition condition between STATE and STATE equals d Let x  a b b d    be a string in that includes STATE  and STATE  as the fourth and fifth vertices in its accepting run  The property is
♦ d  and therefore and x Suppose generalizes      STATE
□ a STATE  from d to  d   c  where   is c  which adds the string x'    a b  b  c to
-
Then If the string suffix after a b b c does not included then there is now a string that includes the trigger but does not include the response  In other words x' Finally if and to an extra check is made to be sure because an atom could be both a response and a trigger  New triggers should be avoided The second part of the algorithm states that if by generalization  then the operator is  safe" to do  It is guaranteed to be safe in this case because if then a response be required here  In other words because for every string in       whose accepting run includes   1  3   either no trigger occurred prior to visiting 1 or every trigger was followed by a response prior to visiting 1 or a response occurred after visiting 3 gen - R is sound but not complete for full Response properties  Its soundness is based on the fact that gen does not increase accessibility of vertices or atoms visited after state 3 i e globally and therefore reverification can be localized to only    κ    1    3 gen - R
is not complete because it may output  Avoid this instance of  gen " when in fact  gen the algorithm will output  Avoid this is safe to do  For example if but instance of gen " Yet it may be the case that '         if no trigger   precedes response    in or if a response is after  3  When    gen-R outputs verification failure  it does not supply sufficient information for FSA repair  Errors must be resolved by selecting another learning operator  Note that  error" has a different connotation for    gen-R than for the AT verification algorithms Any Avoid " output is considered an error Another disadvantage of    gen-R is that it does not allow generalizations that add triggers If it is desirable to add new triggers during generalization then one needs to modify gen-R to call       AT  when reverification with      gen-R fails  instead of outputting   Avoid this instance of  gen "  This modification also fixes the false error problem preserves the enormous time savings  see Section       when reverification succeeds

## 6.4 Theoretical Worst-Case Time Complexity Analysis

Recall that one of our primary objectives is timely agent responses This section compares the worst case time complexity of the algorithms  Let us begin with the time complexity prod  This is i 
*   to form the product of the individual of agent FSAs for Invariance property verification  and
*
to form the product for AT verification Here is the number of agents in is the number of states in single agent FSA 
and is the total number of atoms  multiagent actions   The reason for this complexity result is that there are ff=1 product states for Invariance property verification  and