GPU Accelerated counterexample generation in LTL model checking

• Main Authors: WU, Zhimin, LIU, Yang, LIANG, Yun, SUN, Jun
• Format: text
• Language: English
• Published: Institutional Knowledge at Singapore Management University 2014
• Subjects: Model Check; Share Memory; Task Schedule; Strongly Connect; Component; Model Check Problem; Software Engineering
• Online Access: https://ink.library.smu.edu.sg/sis_research/4988; https://ink.library.smu.edu.sg/context/sis_research/article/5991/viewcontent/gpu.pdf
• Institution: 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...