scholarly journals CCMC: A Conditional CSL Model Checker for Continuous-Time Markov Chains

2013 ◽  
pp. 464-468 ◽  
Author(s):  
Yang Gao ◽  
Ernst Moritz Hahn ◽  
Naijun Zhan ◽  
Lijun Zhang
Keyword(s):  
Markov Chains ◽  
Continuous Time ◽  
Model Checker ◽  
Continuous Time Markov Chains

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

2014 ◽  
Vol 2014 ◽  
pp. 1-6
Author(s):  
Kemin Wang ◽  
Yongbin Wang ◽  
Zhengtao Jiang ◽  
Wenlong Fu
Keyword(s):  
Model Checking ◽  
Markov Chains ◽  
Continuous Time ◽  
Model Construction ◽  
Model Checker ◽  
State Explosion ◽  
Truncation Method ◽  
Continuous Time Markov Chains ◽  
System Properties ◽  
Infinite State

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.

scholarly journals Trace Machines for Observing Continuous-Time Markov Chains

2006 ◽  
Vol 153 (2) ◽  
pp. 259-277 ◽  
Author(s):  
Verena Wolf ◽  
Christel Baier ◽  
Mila Majster-Cederbaum
Keyword(s):  
Markov Chains ◽  
Continuous Time ◽  
Continuous Time Markov Chains

Bounds and Approximations for the Transient Behavior of Continuous-Time Markov Chains

1989 ◽  
Vol 3 (2) ◽  
pp. 175-198 ◽  
Author(s):  
Bok Sik Yoon ◽  
J. George Shanthikumar
Keyword(s):  
Markov Chains ◽  
Continuous Time ◽  
First Passage Time ◽  
Transient Behavior ◽  
Passage Time ◽  
Lower And Upper Bounds ◽  
Simple Method ◽  
Continuous Time Markov Chains ◽  
Recent Addition ◽  
Dependent Probability

Discretization is a simple, yet powerful tool in obtaining time-dependent probability distribution of continuous-time Markov chains. One of the most commonly used approaches is uniformization. A recent addition to such approaches is an external uniformization technique. In this paper, we briefly review these different approaches, propose some new approaches, and discuss their performances based on theoretical bounds and empirical computational results. A simple method to get lower and upper bounds for first passage time distribution is also proposed.

Sign in / Sign up

Export Citation Format

Share Document