The objective of this work is to show the special characteristics of asynchronous concurrent
systems and motivate the necessity of developing specialized traversal algorithms for them.
To fulfill this objective we will perform a comparative study between some of the most common
existing traversal strategies and a number of strategies specially developed for asynchronous
systems. A number of tools have been selected for that comparison. On one side
NuSMV [
1] and VIS [
8],
and on the other side TranSyT [
7], a formal verification tool specialized for
asynchronous systems.
The results will highlight the importance of properly selecting the verification tool according
to the type of system being analyzed. We will show that, in general, verification time can be
greatly reduced, and in some cases specialized techniques will dictate the difference between
enabling an efficient verification or collapsing the capabilities of the selected computer.