Suppose there are n agents, and 1   jk    the number of states in the FSA for agent k. Then the algorithm forms all product states v = ( vjl, .., vj,,) and specifies their transitions:
Procedure product for each product state v = ( vjl, ., vjn ) do if all v jk , 1  k   n, are initial states, then v is a product initial state endif for each multiagent action a; do if ( δ ( v j k , a i ) == 0) for some k , 1    k    n, then δ ( v , a i ) = 0 else δ(ν, α,) = (δ(ν j 1 , α,), ..., δ(ν j n, α,)); endif end for endfor end procedure Figure prod product algorithm T to R i e crt drt in Table This set is expressed in Boolean algebra as I receive L transmit   see Figure For multplans prior to verification the multiagent product FSA needs to lplan Ol be formed from the individual agent FSAs  see Figure      We can implement the algorithm prod for generating the product FSA using the data structure of Table   as shown in Figure     In the product FSA  an example product state and transition is   CRT  drt DR because   C  drt     D    R  drt     D  and   T  drt     R for agents F  I  and L
respectively  The initial states of the product FSA are formed by testing whether every individual state of the product is an initial state  For example  if D  D  and R are initial states for F_I_and_L_respectively_then_DDR_will be an initial state for F__I___L_After forming the product states and specifying which are initial the algorithm of Figure specifies the transition for every product state and multiagent action Note that the algorithm in Figure    forms the product FSA   for testing Invariance properties  To test First Response properties using AT verification  we need to form the To do this simply requires considering      to be the product FSA
st agent The algorithm in Figure is modified by changing   to everywhere It is also important to note that in situations including lagent         prod must be executed iiiiir to form the product is just the single agent FSA and   is    For lan        also  In other words  for lplan the multiagent plan  once formed  is never subdivided and therefore it could be considered like a single agent plan  In both of these cases  if AT verification is done the product is taken of the single plan FSA and the property FSA
Given that the product FSA has been formed if needed  then the final  multi agent FSA
can be verified  We first consider a very simple model checking algorithm  called to tailored specifically for verifying Invariance properties of the form □
The algorithm shown in Figure      consists of a depth first search of    beginning in each initial state   Any accessible atom i that is part of a transition condition  where i violates the property We store the set of all atoms j for rapid access