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

Computer Engineering & Science

Previous Articles     Next Articles

Implementation and optimization of 
LTL probabilistic model checker

LIN Zhe-chao,DONG Wei   

  1. (College of Computer,National University of Defense Technology,Changsha 410073,China)
  • Received:2015-10-14 Revised:2015-12-02 Online:2017-05-25 Published:2017-05-25

Abstract:

Probabilistic model checking is one model checking technology, which cannot only verify the system qualitatively but also judge if the system satisfies quantitative properties. The complexity for LTL probabilistic model checking can be up to a double exponential level. Existing tools such as PRISM and MRMC do not support the validation of LTL properties. We optimize the LTL probabilistic model checking algorithm and implement an efficient LTL model checker. The proposed tool is evaluated via some comparative experiments.
 

Key words: LTL, probabilistic model checking, optimization