GPU Accelerated counterexample generation in LTL model checking

• المؤلفون الرئيسيون: WU, Zhimin, LIU, Yang, LIANG, Yun, SUN, Jun
• التنسيق: text
• اللغة: English
• منشور في: Institutional Knowledge at Singapore Management University 2014
• الموضوعات: Model Check; Share Memory; Task Schedule; Strongly Connect; Component; Model Check Problem; Software Engineering
• الوصول للمادة أونلاين: https://ink.library.smu.edu.sg/sis_research/4988; https://ink.library.smu.edu.sg/context/sis_research/article/5991/viewcontent/gpu.pdf
• المؤسسة: Singapore Management University

Strongly Connected Component (SCC) based searching is one of the most popular LTL model checking algorithms. When the SCCs are huge, the counterexample generation process can be time-consuming, especially when dealing with fairness assumptions. In this work, we propose a GPU accelerated counterexamp...