Suppose there are n agents, and agent i was modified, 1    i    n Operator Ochange modified δ(vi, aadape) to be wi,' for state vi and multiagent action agdapt 1 Then the algorithm is:
Procedure product for each product state v = ( v j 1 , ..., v i , ..., v j n ) formed from state v i do if ( δ ( V j k , α adapl ) == 0) for some k , 1     k     n, then δ ( v, α dapl ) = 0 else δ(v, a adape) = (δ(v j 1, a adapt),..., w i ′ , ..., δ(v j n, a ape)); endif endfor end procedure Figure prod product algorithm AT are sound and complete for r and ible as a Buchi FSA and they find all verification errors Before elaborating on this first note that the term verification error" has a different connotation for
, and l an error is an accessible bad atom  ie   an atom   
For where the property is AT it is an accessible bad state that is part of a cycle  The reason
□
For is sound is that it flags as errors only those atoms It is complete and finds all errors bbecause it does exhaustive search and testing of all accessible atoms AT is also sound to and complete  for analogous reasons  Because I and AT find all errors they can be used with either method of error resolution i e choose another operator or fix the FSA

## 6.2 Incremental Algorithms For  Change And All Situations

All of the algorithms in the previous subsection can be streamlined given that it is known that a learning operator  in this case   change  has been applied  For simplicity  all of our algorithms assume  change is applied to a single atom  multiagent action   For example we assume that if i' where i and i' are implying no next state   and  adapt is a multiagent action   Since we use the states or tabular representation this translates to changing one table entry Figure shows an incremental version of        prod  called      prod  which is tailored for re forming the product FSA after  change has been applied  The algorithm of Figure is for Invariance properties  for AT verification change    to st agent  Although     prod is applicable in all situations when taking the is the product with the property FSA  the primary motivation for developing this algorithm was the multiagent       multplans  Recall that in this situation  every time learning is applied to an individual agent FSA  the product must be    formed to verify global properties  The wasted cost of doing this motivated the development of this algorithm Algorithm prod assumes that the product was formed originally  before learning prod capitalizes on the knowledge of what  individual or multiagent using prod state     and multiagent action   adapt  transition to a new next state as specified by operator  change  This algorithm assumes that the prelearning product FSA is stored  Then the only product FSA states whose next state needs to be modified are those states that