Let us consider the results in Tables   and    In both of these tables  each row corre sponds to an algorithm Rows are numbered for later reference The entries give perfor mance results to be described shortly  Table   compares the performance of total rever ication with the algorithms of Subsection     which were designed for  change and situations  The situation assumed for these experiments was     multplans  Three dense random  subject to the above mentioned restrictions  FSAs were generated  and then the product was formed  The result was a product FSA satisfying the property  Operator change was then applied which consisted of a random  but points to a state instead of change to a randomly chosen table entry in the FSA transition table for a random choice of one of the three agents  Finally  the product FSA was re formed and reverification done The methodology for generating Table   was similar to that for Table except that gen was the learning operator and the situation was assumed to be lplan  In other words the product FSA was formed and then gen applied to the FSA of the three agents the product was taken with the property FSA if needed for AT verification and then reverification performed  Operator  gen consisted of choosing a random state  ; and a random action and then setting Any column in Tables or labeled sec" gives a mean over   runs of the cpu time of the algorithm Columns labeled spd" give the speedup over total ie the cpu time of the incremental algorithm in that row divided by the cpu time of the corresponding total algorithm  For example the  spd" entry for    prod in row   gives its cpu time divided by the cpu time of prod in row    Columns labeled  err" show the average number of verification errors over    runs  This is important to monitor because  for example  the cpu time is most strongly correlated with the number of states  visited" during dfs  and visited " during ndfs when AT verification is used  Every property error causes ndfs to be called with a nested search  which may be quite time consuming  Also  it is important to note that we did not force any verification errors to occur  It was our objective to monitor cpu time under natural circumstances for evolving FSAs  When errors arose they were the natural result of applying a learning operator  The  err" columns are missing from Table because the values are all i e no errors occurred during the experiments due to applying  change  although we have observed errors to occur with this operator not during the experiments   The lack of errors in the experiments resulted from the particular random FSAs that happened to be generated during the experiments  Errors are quite common with the specific gen version of change as can be seen in Table Note that N A" is in the  err" column for anything other than a verification algorithm because  err" refers to verification errors The algorithms  rows  should be considered in triples  p "  v " and  b " or else as a single item _v_b "_A__p" next to an algorithm name in Table__or__denotes it is a product algorithm a v" that it is a verification algorithm and a b" that it is the sum of the p" and  v" entries  ie   the time for        re forming the product and reverifying   For example 1 b  is considered to be an algorithm pair consisting of of Table      If no product needs to be formed  then the   b" version of the v   see rows algorithm is identical to the  v" version  in which case there is only one row labeled   v   b "
present a subset  cpu time only  of the data from Tables   and Tables and in a format that facilitates some comparisons  In other words  Tables and contain