Available results demonstrates that for asynchronous systems the selection of a conjunctive partitioned TR is clearly inappropriate. Table 3 shows several orders of magnitude in the number of BDD nodes required to represent TRs. This is true because in a disjunctive partition all variables that should not change the state can be eliminated from the support of the TR, and also from the set of variables that should be quantified. Adding these ``equivalence'' factors in the conjunctive representation complicates the BDD representation.
Tables 4, and 5, show that even a BFS traversal scheme can be reasonably efficient if used in combination with a disjunctive representation of the TR. CPU times are far from being efficient, but at least mid-size examples can be completed. Using the chaining technique drastically improves the traversal process consistently across all benchmarks. It is not clear, however, the particular heuristic that will provide better result on each example. Further analysis is required in order to try to classify systems according the traversal strategy to be applied.
It is interesting to note that TranSyT performs consistently well with a good starting variable order and with or without automatic reorder activated. However, NuSMV and VIS perform significantly better when automatic reordering is available. We believe that this is because the initial variable orders were designed to minimize the size of the reachability sets, and in both NuSMV and VIS the size of the TR is the dominant BDD factor.