SKLCS Seminar 

　　Title: An I/O Efficient Approach for Detecting All Accepting Cycles 

　　Speaker: Lijun Wu (University of Electronic Science and Technology, Chengdu) 

　　Time: 10:00, April 21, 2016 

　　Venue: Seminar Room (334), Level 3, Building 5, Institute of Software, Chinese Academy of Sciences. 

　　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). 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. 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. 

　　Biography: 

　　Lijun Wu is a professor in the Department of Computer Science at University of Electronic Science and Technology, Chengdu. He received the Ph.D in Computer Science from Sun Yat Sen University in 2005. His research interests include formal methods and multi-agent systems. In particular, his recent interest is I/O efficient approach to model checking, and his works in this line has been published on journals such as IEEE Transactions on Software Engineering and IEEE Transactions on VLSI Systems.