Stochastic Automata Networks and Lumpable Stochastic Bounds: Bounding Availability

The use of Markov chains to model complex systems is becoming increasingly common in many areas of science and engineering. The underlying transition matrix of the Markov chain can frequently be represented in an extremely compact form – a consequence of the manner in which the matrix is generated. This means that the definition and generation of large-scale Markov models is relatively easy and efficient in both time and memory requirements. The remaining difficulty is that of actually solving the Markov chain and deriving useful performance characteristics from it.

The use of bounding procedures is one approach to alleviating this problem. Such bounds are frequently more easily obtained than the exact solution and provide sufficient information to be of value. In this chapter, we show how to bound certain dependability characteristics such as steady-state and transient availability using an algorithm based on the storage of the Markov chain as a sum of tensor products. Our bounds are based on arguments concerning the stochastic comparison of Markov matrices rather than the usual approach which involves sample-path arguments. The algorithm requires only a small number of vectors of size equal to the number of reachable states of the Markov chain.