Parallel and Distributed Algorithms for Model Checking Problems (Doctoral Consortium)

State space explosion is the main challenge in model checking problems. On-the-fly verification, partial order reduction and stuttering equivalence are the three major solutions for this problem, which have drawn a lot of attention. While most researches work with sequential algorithms, for which their performance is also restricted by the size of state space. As the algorithms for model checking problems can always be regarded as the graph exploration or matrix operations, utilizing parallel computing to deal with the model checking problems has been a significant topic. It can benefit from the high computation capability and high memory size of different parallel and distributed platforms, e.g., multi-core CPU, manycore GPU, cluster and cloud. However, we should face several challenges to integrate parallel computing into model checking area: 1) The construction of the high efficiency data structure for system models to save memory cost and being efficient for parallel accessing. 2) The development of efficient execution model with high computation locality. For property verification, it is necessary to verify the correctness of the parallel and distributed property verification process. 3) The implementations should follow the up-to-date features of different platforms. Our researches are to build approaches to deal with several model checking problems with parallel computing in multi-core and many-core platforms, which involves how to fight for the challenges.