A Multistep Extending Truncation Method towards Model Construction of Infinite-State Markov Chains. (24th December 2013) - Wang, Kemin; Wang, Yongbin; Jiang, Zhengtao; Fu, Wenlong
Abstract : 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.