• 中国计算机学会会刊
  • 中国科技核心期刊
  • 中文核心期刊

Computer Engineering & Science

Previous Articles     Next Articles

Symbolic CTL model checking based on possibility measure

LEI Lihui,GUO Yue,ZHANG Yanbo   

  1. (College of Computer Science,Shaanxi Normal University,Xi’an 710119,China)
  • Received:2018-06-09 Revised:2018-08-24 Online:2018-11-25 Published:2018-11-25

Abstract:

With the increasing complexity of systems, it is urgent to deal with the uncertain information in the systems. Besides, the state explosion problem is getting more and more serious. Existing model checking techniques are no longer suitable for the verification of such complex systems. We study symbolic CTL model checking based on possibility measure. Firstly, multiterminal binary decision trees (MTBDDs) and Boolean formula are respectively used to describe system models and properties to be verified. Secondly, the system models are normalized and simplified. Finally, system verification is completed by fixed point calculation. Our work is an integration of symbolic model checking and CTL model checking based on possibility measure, which can not only handle uncertain information in systems, but also maintain symbolic model checking's advantage of low demand for computation time and storage space. It is thus significant for the verification of complex systems.
 

Key words: symbolic model checking, possibility measure, CTL;MTBDD