Irreducible Markov Regenerative Processes (MRP) 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. This paper 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. The paper 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 CSLTA reduces to that of CSL if the component method is used.

A component-based solution for reducible Markov regenerative processes

AMPARORE, ELVIO GILBERTO;DONATELLI, Susanna
2012

Abstract

Irreducible Markov Regenerative Processes (MRP) 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. This paper 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. The paper 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 CSLTA reduces to that of CSL if the component method is used.
70
400
422
Markov regenerative process; CTMC; component-based solution; Stochastic Model Checking
Elvio Gilberto Amparore; Susanna Donatelli
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/2318/148131
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 14
  • ???jsp.display-item.citation.isi??? 10
social impact