[ZhangHHW08]
Time-bounded model checking of infinite-state continuous-time Markov chains
In 8th International Conference on Application of Concurrency to System Design (ACSD), pages 98-107, IEEE, 2008.
Downloads: pdf, bibURL: http://dx.doi.org/10.1109/ACSD.2008.4574601
Abstract. 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 experimental evidence
showing that our method is effective.