Evaluating symbolic traversal algorithms applied to asynchronous concurrent systems

Symbolic reachability analysis based on binary decision diagrams (BDDs) is a technique that allows the implementation of efficient invariant checking algorithms, and improves the performance of CTL/LTL verification. However, in practice it is well known that the BDD blowup problem limits the size of the systems that can be successfully verified. Along the years multiple variants of the basic reachability scheme have been introduced. However, most of them perform nicely only on synchronous systems or under the assumption that the transition relation (TR) can be effectively decomposed as a conjunction. This paper intends to demonstrate that the reachability algorithms based on these premises do not fit properly on asynchronous concurrent systems. Therefore it justifies developing alternative reachability algorithms for concurrent systems, or even for mixed synchronous/asynchronous schemes.