Bounded Model Checking for Probabilistic Computation Tree Logic
Author:
Affiliation:

  • Article
  • | |
  • Metrics
  • |
  • Reference [21]
  • |
  • Related [20]
  • |
  • Cited by
  • | |
  • Comments
    Abstract:

    In order to overcome the state explosion problem in model checking the probabilistic computation tree logic, a bounded model checking technique is proposed. First, the bounded semantics of the probabilistic computation tree logic is presented, and then its correctness is proved. Second, by a simple instance the criterion of the traditional termination, based on the length of path, is shown to fail. Based on the termination criterion used in the Newton iteration in numerical computing, a new criterion is given. Third, the bounded model checking procedure of the probabilistic computation tree logic is transformed into linear equations. Finally, three benchmarks are used to present the advantages of the bounded model checking.

    Reference
    [1] Alur R. Model checking: From tools to theory. Lecture Notes in Computer Science, 2008,5000:89-106. [doi: 10.1007/978-3-540-69850-0_6]
    [2] Lin HM, Zhang WH. Model checking: Theories, techniques and applications. Acta Electronica Sinica, 2002,30(12A):1907-1912(in Chinese with English abstract).
    [3] Hansson H, Jonsson B. A logic for reasoning about time and reliability. Formal Aspects of Computing, 1994,6(5):512-535. [doi:10.1007/BF01211866]
    [4] Baier C, Katoen JP. Principles of Model Checking. Cambridge: MIT Press, 2008. 745-907.
    [5] Kattenbelt M, Kwiatkowska M, Norman G, Parker D. A game-based abstraction-refinement framework for Markov decisionprocesses. Formal Methods in System Design, 2010,36(3):246-280. [doi: 10.1007/s10703-010-0097-6]
    [6] Clarke EM. My 27-year quest to overcome the state explosion problem. In: Pitts A, ed. Proc. of the 24th Annual IEEE Symp. onLogic in Computer Science. Washington: IEEE Computer Society, 2009. 3. [doi: 10.1109/LICS.2009.42]
    [7] Clarke EM, Grumberg O, Jha S, Lu Y, Veith H. Progress on the state explosion problem in model checking. Lecture Notes inComputer Science, 2001,2000:176-194. [doi: 10.1007/3-540-44577-3_12]
    [8] Bryant RE. Graph-Based algorithms for boolean function manipulation. IEEE Trans. on Computers, 1986,35(8):687-691. [doi:10.1109/TC.1986.1676819]
    [9] Burch JR, Clarke EM, McMillan KL. Symbolic model checking: 1020 states and beyond. Information and Computation, 1992,98(2):142-170. [doi: 10.1016/0890-5401(92)90017-A]
    [10] Su KL, Luo XY, Lu GF. Symbolic model checking for CTL. Chinese Journal of Computers, 2005,28(11):1798-1806 (in Chinesewith English abstract).
    [11] Qu WX, Li T, Guo Y, Yang XD. Advances in predicate abstraction. Journal of Software, 2008,19(1):27-38 (in Chinese withEnglish abstract). http://www.jos.org.cn/1000-9825/19/27.htm [doi: 10.3724/SP.J.1001.2008.00027]
    [12] Wolper P, Godefroid P. Partial order methods for temporal verification. Lecture Notes in Computer Science, 1993,715:233-246.[doi: 10.1007/3-540-57208-2_17]
    [13] Emerson EA, Sistla AP. Symmetry and model checking. Formal Methods in System Design, 1996,9(1):105-131. [doi: 10.1007/BF00625970]
    [14] Pasareanu CS, Dwyer MB, Huth M. Assume-Guarantee model checking of software: A comparative case study. Lecture Notes inComputer Science, 1999,1680:168-183. [doi: 10.1007/3-540-48234-2_14]
    [15] Biere A, Cimatti A, Clarke EM, Zhu Y. Symbolic model checking without BDDs. Lecture Notes in Computer Science, 1999,1579:193-207. [doi: 10.1007/3-540-49059-0_14]
    [16] Yang JJ, Su KL, Luo XY, Lin H, Xiao YY. Optimization of bounded model checking. Journal of Software, 2009,20(8):2005-2014(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/3387.htm [doi: 10.3724/SP.J.1001.2009.03387]
    [17] Luo XY, Su KL, Yang JJ. Bounded model checking for temporal epistemic logic in synchronous multi-agent systems. Journal ofSoftware, 2006,17(12):2485-2498 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/17/2485.htm [doi: 10.1360/jos172485]
    [18] Zhang WH. Model checking with SAT-based characterization of ACTL formulas. Lecture Notes in Computer Science, 2007,4789:191-211. [doi: 10.1007/978-3-540-76650-6_12]
    [19] Zhang WH. Bounded semantics of CTL and SAT-based verification. Lecture Notes in Computer Science, 2009,5885:286-305. [doi:10.1007/978-3-642-10373-5_15]
    [20] Xu L, Chen W, Xu YY, Zhang WH. Improved bounded model checking for universal fragment of CTL. Journal of Computer Science and Technology, 2009,24(1):96-109. [doi: 10.1007/s11390-009-9208-5]
    [21] Penna GD, Intrigila B, Melatti I, Tronci E, Zilli MV. Bounded probabilistic model checking with the Murφ verifier. Lecture Notes in Computer Science, 2004,3312:214-229. [doi: 10.1007/978-3-540-30494-4_16]
    Cited by
Get Citation

周从华,刘志锋,王昌达.概率计算树逻辑的限界模型检测.软件学报,2012,23(7):1656-1668

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:October 05,2010
  • Revised:July 08,2011
  • Online: July 03,2012
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063