Computer Science ›› 2018, Vol. 45 ›› Issue (4): 71-75.doi: 10.11896/j.issn.1002-137X.2018.04.010

Previous Articles     Next Articles

Parallelization of LTL Model Checking Based on Possibility Measure

LEI Li-hui and WANG Jing   

  • Online:2018-04-15 Published:2018-05-11

Abstract: 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.

Key words: Possibilistic Kripke structure,State partition of system,Quantitative distributed model checking

[1] BAIER C,KATOEN J P.Principles of model checking[M].Cam-bridge:The MIT Press,2008.
[2] LI Y M,DROSTE M,LEI L H.Model checking of linear-time properties in multi-valued system[J].Information Sciences,2017,7:51-74.
[3] KHOUSSAINOV B,NERODE A.Automata Theory and its Ap-plications[M].Birkauser,2001.
[4] LI Y M,LI L J.Model checking of linear- time properties based on possibility measure [J].IEEE Transaction on Fuzzy Systems,2013,1(5):842-854.
[5] LI L,LI J.Model-checking of linear-time properties in possibilistic Kripkestructure [C]∥Quanitative Logic and Soft Computing-the QI&SC.2012:287-294.
[6] LI Y M.Two methods for Model-checking ofLTL[J].Journal of Shaanxi Normal University(Natural Science Edition),2014,42(4):22-25.(in Chinese) 李永明.可能LTL模型检测的两种方法[J].陕西师范大学学报(自然科学版),2014,2(4):22-25.
[7] LI L J.Model checking of linear-time properti-es based on possibility measure [D].Xi’an:Shaanxi Normal University,2012.(in Chinese) 李丽君.基于可能性测度的LTL 模型检测[D].西安:陕西师范大学,2012.
[8] EDMUND E,GRUMBERG O,PELED D.Model checking [M].Cambridge:The MIT Press,1999.
[9] EVANGELISTA Y M,PRADAT-PEYRE J F.Memory Efficient State Space Storage in Explicit Software[C]∥InternationalSpin Workshop on Model Checking of Software.2005:43-57.
[10] BARNAT J,BRIM L,ROCKAI P.Scalable multicore LTL modelchecking[M]∥ Model Checking Sofware.Springer Berlin Heidelberg,2007:187-203.
[11] HOU G,ZHOU K J,YONG J W,et al.Research overview of state explosion in the model checking[J].Computer Science,2013,0(6A):77-86.(in Chinese) 候刚,周宽久,勇嘉伟,等.模型检测中状态爆炸问题研究综述[J].计算机科学,2013,0(6A):77-86.
[12] JIANG Y X,LIN C,XING X J.Model checking of Petri netbased on linear logic[J].Journal of System Simulation,2003,15(21):6-10.(in Chinese) 蒋屹新,林闯,刑栩嘉.基于线性逻辑的Petri 网的模型检测[J].系统仿真学报,2003,5(21):6-10.
[13] BOURAHLA M.Distributed CTL model checking[J].IEEEProceedings Software,2005,2(6):297.
[14] LERDA F,SISTO R.Distributed-memory model checking with spin[C]∥International Spin Workshops on Theoretical & Practical Aspects of Spin Model Checking.Spinger-Verlag,1999:22-39.
[15] BARNAT J,BRIM L,STˇBRN J.Distributed LTL model-checking in SPIN[C]∥Proceedings of the 8th International SPIN Workshop on Model Checkingof Software.2001:200-216.

No related articles found!
Full text



No Suggested Reading articles found!