%A LEI Li-hui and WANG Jing %T Parallelization of LTL Model Checking Based on Possibility Measure %0 Journal Article %D 2018 %J Computer Science %R 10.11896/j.issn.1002-137X.2018.04.010 %P 71-75 %V 45 %N 4 %U {https://www.jsjkx.com/CN/abstract/article_4.shtml} %8 2018-04-15 %X Distributed model checking(DMC) is an effective solution for the state-explosion problem in model checking.The qualitative LTL distributed model verification algorithm has been proposed.However,the problem of parallelization quantitative LTL verification has not been solved effectively.In this paper,a new dynamic state partition method was presented and a quantitative DMC was proposed based on the qualitative LTL distributed verification algorithm.Firstly,the system model is transformed into a possible Kripke structure to choose a concurrent component,and its state space is divided by the relationships of states,which aims to allocate the related states to the same computing node.Secondly,the partition results are adjusted for the load balance of DMC system.Then,the partition results and the states of the rest components are done cross product to complete the state partition of the system.Finally,the properties are represented by nondeterministic finite automaton,and their cross products can complete the quantitative verfication of system based on the extended nested DFS distributed verification algorithm.