We give a brief overview of the traversal methods implemented in three selected verification tools: NuSMV, VIS and TranSyT. The first is a well known verification tool [1] basically aimed to synchronous verification, although its language allows the specification of asynchronous concurrent systems. VIS [8] it is also a well known tool but its input language is much more synchronous circuit oriented, although it is possible to translate deterministic asynchronous systems to this kind of representation. On the other hand, TranSyT [7] is completely oriented to concurrent system verification. All tools use the same underlying data structure (BDDs) but have exponential different running times when computing the reachability set of several concurrent systems