Sciweavers

ACSD
2008
IEEE

Time-bounded model checking of infinite-state continuous-time Markov chains

14 years 2 days ago
Time-bounded model checking of infinite-state continuous-time Markov chains
The design of complex concurrent systems often involves intricate performance and dependability considerations. Continuous-time Markov chains (CTMCs) are widely used models for concurrent system designs making it possible to model check such properties. In this paper, we focus on probabilistic timing properties of infinite-state CTMCs, expressible in continuous stochastic logic (CSL). Such properties comprise important dependability measures, such as timed probabilistic reachability, performability, survivability, and various availability measures like instantaneous availabilities, conditional instantaneous availabilities and interval availabilities. Conventional model checkers explore the given model exhaustively which is not always possible either due to state explosion or because the model is infinite. This paper presents a method that only explores the infinite (or prohibitively large) model up to a finite depth, with the depth bound being computed on-the-fly. We provide experimen...
Lijun Zhang, Holger Hermanns, Ernst Moritz Hahn, B
Added 12 Oct 2010
Updated 12 Oct 2010
Type Conference
Year 2008
Where ACSD
Authors Lijun Zhang, Holger Hermanns, Ernst Moritz Hahn, Björn Wachter
Comments (0)