| ¡¡ | Chinese Journal of Computers Full Text |
| Title | Truly Bitstate-Hashing for SCC-Based Emptiness Checking Algorithms |
| Authors | YAN Rong-Jie1),2) ZHANG Wen-Liang1),2) TANG Zhi-Song1) |
| Address | 1)(State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100190) 2)(Graduate University of Chinese Academy of Sciences, Beijing 100039) |
| Year | 2008 |
| Issue | No.6(979¡ª988) |
| Abstract & Background | Abstract The paper proposes an improvement for SCC-based emptiness checking algorithms, which combines the advantages of SCC-based and nested depth first search for finding a cycle meeting all sets of acceptance conditions. The new algorithm uses the method of bitstate-hashing during emptiness checking for transition-based generalized B¨¹chi automata, and the performance outperforms that of Couvreur¡¯s. Meanwhile, the performance for finding a counterexample is the same as that of SCC-based ones. Keywords emptiness checking; transition-based generalized B¨¹chi automaton; acceptance conditions Background The projects are the fundamental research of computer software theory, which aims to ensuring the correctness and reliability of safety critical systems by formal methods. Automata-theoretic approach is one of the effective methods to ensure the correctness of concurrent systems. The verification of linear temporal logic (LTL) formulas relies on an algorithm for finding accepting cycles in the product of the system and a B¨¹chi automaton for the negation of the formula, which reduces to the checking of emptiness of a product B¨¹chi automaton. State space explosion is deteriorated in emptiness checking. Though many related algorithms have made some improvements, there is hardly a balance between the time and memory consumption for the emptiness checking. The authors¡¯ objective is to improve the time performance and reduce the memory consumption during the emptiness checking for linear temporal logic formulas. The paper proposes an improvement for SCC-based emptiness checking algorithms, which combines the advantages of SCC-based and nested depth first search for finding a cycle meeting all sets of acceptance conditions. The work in this paper will enrich the methodology research in our projects. Their group has made some progresses on the algorithms and symbolic data structures to relieve the problem of state space explosion, and developed several model checking tools during the years of research, which can be downloaded from the website. |