A Multistep Extending Truncation Method towards Model Construction of Infinite-State Markov Chains

作者:Wang Kemin*; Wang Yongbin; Jiang Zhengtao; Fu Wenlong
来源:Mathematical Problems in Engineering, 2014, 2014: 764819.
DOI:10.1155/2014/764819

摘要

The model checking of Infinite-State Continuous Time Markov Chains will inevitably encounter the state explosion problem when constructing the CTMCs model; our method is to get a truncated model of the infinite one; to get a sufficient truncated model to meet the model checking of Continuous Stochastic Logic based system properties, we propose a multistep extending advanced truncation method towards model construction of CTMCs and implement it in the INFAMY model checker; the experiment results show that our method is effective.

  • 出版日期2014
  • 单位中国传媒大学

全文