A structured path-based approach for computing transient rewards of large CTMCs

Structured (a.k.a. symbolic) representation techniques of Markov models have, to a large extent, been used effectively for representing very large transition matrices and their associated state spaces. However, their success means that the largest space requirement encountered when analyzing these models is often the representation of their iteration and solution vectors. In this paper, we present a new approach for computing bounds on solutions of transient measures in large continuous-time Markov chains (CTMCs). The approach extends existing path- and uniformization-based methods by identifying sets of paths that are equivalent with respect to a reward measure and related to one another via a simple structural relationship. This relationship allows us to explore multiple paths at the same time, thus significantly increasing the number of paths that can be explored in a given amount of time. Furthermore, the use of a structured representation for the state space and the direct computation of the desired reward measure (without ever storing the solution vector) allow us to analyze very large models using a very small amount of storage. In addition to presenting the method itself, we illustrate its use to compute the reliability and the availability of a large distributed information service system in which faults may propagate across subsystems.