Combining Couvreur´s Algorithm with Bitstate-Hashing for Emptiness Check

Emptiness check is very important in model checking to LTL. In this paper we first present a new emptiness checking algorithm, which is based on Couvreur´s algorithm, to make it be compatible with bitstate-hashing completely. And then we show the correctness of the improved algorithm by analyzing it and Couvreur´s algorithm. At last, we make the experiment to compare the improved algorithm to several known algorithms, which will show its interaction with bitstate-hashing completely while keeping the performance on the whole. This expands the usefulness of Couvreur´s algorithm largely