Name
Abstract | ||
|---|---|---|
The design of complex concurrent systems often involves intricate performance and dependability considerations. Continuous-time Markov chains (CTMCs) are a widely used modeling formalism that captures such performance and dependability properties, and makes them analyzable by model checking. In this paper, we focus on time-bounded probabilistic properties of infinite-state CTMCs, expressible in a subset of continuous stochastic logic (CSL). This comprises important dependability measures, such as time-bounded probabilistic reachability, performability, survivability, and various availability measures like instantaneous, conditional instantaneous and interval availabilities. Conventional model checkers explore the given model exhaustively, which is often costly, due to state explosion, and sometimes impossible because the model is infinite. This paper presents a method that only explores the model up to a finite depth. The required depth is determined on the fly by an algorithm that is configurable in order to adapt to the characteristics of different classes of models. We provide experimental evidence showing that our method is effective. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.3233/FI-2009-145 | Fundam. Inform. |
Keywords | DocType | Volume |
finite depth,conditional instantaneous,model checking,time-bounded model checking,infinite-state continuous-time markov chains,infinite-state ctmcs,dependability consideration,intricate performance,dependability property,conventional model checker,model exhaustively,important dependability measure,markov chains,uniformization,truncation | Journal | 95 |
Issue | ISSN | Citations |
1 | 0169-2968 | 5 |
PageRank | References | Authors |
0.46 | 23 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| E. Moritz Hahn | 1 | 16 | 1.68 |
| Holger Hermanns | 2 | 3418 | 229.22 |
| Björn Wachter | 3 | 326 | 20.09 |
| Lijun Zhang | 4 | 451 | 24.40 |