In Search of Probability Mass: Probabilistic Evaluation of High-Level Specified Markov Models

One of the main problems arising when using high-level specification methods to describe system performance and dependability models, be they stochastic Petri nets, stochastic process algebras or queueing networks, is the growth of the state space of the underlying Markov chain. We therefore propose an approach that avoids this problem by only generating those Markov-chain states that really do matter, i.e., those states that contain most of the probability mass. We first describe our approach in a general setting and then propose various ways to selectively explore the state space in order to capture the most important states. The chosen approach allows us to increase the state space size stepwise until a preset level of accuracy is met. We illustrate this so-called probabilistic evaluation approach for transient dependability measures computed via uniformization.