Time-Bounded Model Checking of Infinite-State Continuous-Time Markov Chains
In Fundamenta Informaticae
, 95: 129-155, 2009.
Downloads: pdf, bibURL: http://dx.doi.org/10.3233/FI-2009-145
Abstract. The design of complex concurrent systems often involves intricate
performance and de- pendability 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 de- pendability 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.