Multi-core model checking algorithm development

Model checking is an automatic technique for verifying finite state systems. Strongly Connected Components (SCC) detection is one of the major approaches for LTL Model Checking, which is suitable for fairness assumption. Currently, Tarjan’s Algorithm is a widely used Depth-first search (DFS) process to deal with the SCC detection problem, which has been implemented as sequential algorithms in many tools, e.g. Process Analysis Toolkit (PAT). However, It always costs a lot of time with large-scale system models. In my project, I improve the performance of Tarjan’s algorithm by implementing and optimizing the concurrent Tarjan’s algorithm described in Gavin’s Paper. Different from the algorithm in that paper, I optimize the concurrent Tarjan’s algorithm to build an approach that can support the on-the-fly LTL model checking with fairness assumption in PAT.Bachelor of Engineering (Computer Science