Affiliations: Department of Computer Science Saarland University
Saarbrücken, Germany. E-mail: {zhang,emh,hermanns,bwachter}@cs.uni-sb.de
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.
Keywords: Markov chains, model checking, truncation, uniformization
