An I/O efficient approach for detecting all accepting cycles

Wu, Lijun, Su, Kaile, Cai, Shaowei, Zhang, Xiaosong, Zhang, Chenyi and Wang, Shupeng (2015) An I/O efficient approach for detecting all accepting cycles. IEEE Transactions on Software Engineering, 41 8: 730-744. doi:10.1109/TSE.2015.2411284

Author Wu, Lijun
Su, Kaile
Cai, Shaowei
Zhang, Xiaosong
Zhang, Chenyi
Wang, Shupeng
Title An I/O efficient approach for detecting all accepting cycles
Journal name IEEE Transactions on Software Engineering   Check publisher's open access policy
ISSN 0098-5589
Publication date 2015-08
Sub-type Article (original research)
DOI 10.1109/TSE.2015.2411284
Open Access Status DOI
Volume 41
Issue 8
Start page 730
End page 744
Total pages 15
Place of publication Piscataway, NJ, United States
Publisher Institute of Electrical and Electronics Engineers
Collection year 2016
Language eng
Abstract Existing algorithms for I/O Linear Temporal Logic (LTL) model checking usually output a single counterexample for a system which violates the property. However, in real-world applications, such as diagnosis and debugging in software and hardware system designs, people often need to have a set of counterexamples or even all counterexamples. For this purpose, we propose an I/O efficient approach for detecting all accepting cycles, called Detecting All Accepting Cycles (DAAC), where the properties to be verified are in LTL. Different from other algorithms for finding all cycles, DAAC first searches for the accepting strongly connected components (ASCCs), and then finds all accepting cycles of every ASCC, which can avoid searching for a great many paths that are impossible to be extended to accepting cycles. In order to further lower DAAC's I/O complexity and improve its performance, we propose an intersection computation technique and a dynamic path management technique, and exploit a minimal perfect hash function (MPHF). We carry out both complexity and experimental comparisons with the state-of-the-art algorithms including Detect Accepting Cycle (DAC), Maximal Accepting Predecessors (MAP) and Iterative-Deepening Depth-First Search (IDDFS). The comparative results show that our approach is better on the whole in terms of I/O complexity and practical performance, despite the fact that it finds all counterexamples.
Keyword Breath-first search
Detection of All Accepting cycles
Model checking
Q-Index Code C1
Q-Index Status Confirmed Code
Institutional Status UQ

Document type: Journal Article
Sub-type: Article (original research)
Collections: Official 2016 Collection
School of Information Technology and Electrical Engineering Publications
Version Filter Type
Citation counts: TR Web of Science Citation Count  Cited 0 times in Thomson Reuters Web of Science Article
Scopus Citation Count Cited 0 times in Scopus Article
Google Scholar Search Google Scholar
Created: Tue, 01 Sep 2015, 00:27:33 EST by System User on behalf of Scholarly Communication and Digitisation Service