A component-based solution for reducible Markov regenerative processes

Irreducible Markov Regenerative Processes (MRPs) are solved by either building and storing the embedded DTMC (EMC) beforehand (explicit approach), or by applying implicit techniques, in which the EMC is never computed or stored. The implicit approach usually outperforms the explicit one, both in terms of time and memory. aper introduces an implicit and component-based method for the steady-state solution of reducible Markov regenerative processes: the strongly connected components of the characteristic matrices of the process are used to identify a structure of components that is exploited by the solution process to discriminate components of the process that have a simple or a complex structure, and corresponding lower and higher solution costs. The solution then considers one component at a time, applying to each of them the simplest solution technique adequate to the actual component complexity. An implicit approach is followed, which saves the cost of building and storing the EMC, but makes non trivial the identification of the strongly connected components. per shows the efficacy of the method both in theory and on a set of MRPs arising from queueing networks, stochastic Petri nets and from the stochastic model checking of Markov chains. In particular it is shown that the cost of the model checking of the Until formula of the stochastic logic CSL TA  reduces to that of CSL if the component method is used.