A large variety of computer and communication systems can be modeled adequately as infinite-state continuous-time Markov chains (CTMC).
A highly-structured class of such infinite-state CTMCs is the class of Quasi-Birth-Death processes (QBDs), on which we focus in this paper.
To model check systems that can be modeled as QBDs, we need to calculate the transient probabilities for all, that is, an infinite number
of starting states. In this presentation, we show an efficient variant of uniformization for the transient analysis of QBDs. Although the set of starting states
has potentially an infinite number of elements, our algorithm facilitates the calculation of the transient probabilities for all these starting states.
We present the required data structures and algorithms, as well as an optimal stopping criterion given the measure to be evaluated.
In a simple case study we show that our approach is feasible.