A Multistep Extending Truncation Method towards Model Construction of Infinite-State Markov Chains. (24th December 2013)

• Record Type: Journal Article
• Authors: Wang, Kemin; Wang, Yongbin; Jiang, Zhengtao; Fu, Wenlong
• Other Names: He Shuping Academic Editor.
• Is Part Of: Mathematical problems in engineering. Volume 2014(2014)
• Publication Date: 2013-12-24
• Subjects: Engineering mathematics -- Periodicals; 510.2462
• DOI: 10.1155/2014/764819
• Languages: English
• ISSNs: 1024-123X

Abstract

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.