计算机科学 ›› 2018, Vol. 45 ›› Issue (4): 71-75.doi: 10.11896/j.issn.1002-137X.2018.04.010

• 2017年全国理论计算机科学学术年会 • 上一篇    下一篇

可能性测度下的LTL模型检测并行化研究

雷丽晖,王静   

  1. 陕西师范大学计算机科学学院 西安710062,陕西师范大学计算机科学学院 西安710062
  • 出版日期:2018-04-15 发布日期:2018-05-11
  • 基金资助:
    本文受国家自然科学基金(11271237,11301321),中央高校基本科研业务费专项资金(GK201603086)资助

Parallelization of LTL Model Checking Based on Possibility Measure

LEI Li-hui and WANG Jing   

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

摘要: 分布式模型检测是一种缓解状态空间爆炸的有效途径,已有文献提出了定性的分布式模型验证算法,然而定量LTL验证算法并行化问题还未得到有效解决。对此,展开两个方面的工作:提出一种新的动态系统状态空间划分方法;在定性LTL分布式验证算法的基础上给出了定量模型检测并行化验证算法。首先,将系统模型转化为可能的Kripke结构并选取一个并发分量,依据状态之间的关系完成系统状态的分割,使得关系紧密的状态尽可能分布在同一个计算节点上;其次,调整划分结果以使得计算负载平衡;然后,将划分结果与其他并发分量的状态进行叉乘,以完成系统状态空间的划分;最后,将待检测性质用自动机表示,在两者的乘积上,利用扩展的基于嵌套DFS的分布式验证算法完成系统的定量验证。

关键词: 可能的Kripke结构,状态空间划分,定量分布式模型检测

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!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!