In this paper we investigate the computation, and the stochastic interpretation, of backward probabilities of Markov chains (transient and steady-state probabilities derived from backward Kolmogorov equations) and its extension to the case of Markov Regenerative Processes (MRP). The study is then extended to the case of non-ergodic settings, which enlights a substantial difference between the forward solution process (based on forward Kolmogorov equations) and the backward one. We shall clarify the role that backward solutions play in computing absorption probabilities and in the model- checking of stochastic logics as CSL and CSLTA, which typically require the steady state solution of a non-ergodic CTMC and MRP respectively. Moreover we show that the algorithm for the computation of the whole set of states that satisfy a CSL formula, which is standard practice in CSL model-checkers, can be seen as a case of computation of backward probabilities of Continuous Time Markov Chains (CTMCs). The backward computation of MRP is then inserted in the context of matrix-free solution technique, which allows to deal with MRP of much bigger size than the standard approach based on the computation and solution of the embedded Markov chain.

Backward solution of Markov chains and Markov Renewal Processes: formalization and applications

AMPARORE, ELVIO GILBERTO;DONATELLI, Susanna
2012

Abstract

In this paper we investigate the computation, and the stochastic interpretation, of backward probabilities of Markov chains (transient and steady-state probabilities derived from backward Kolmogorov equations) and its extension to the case of Markov Regenerative Processes (MRP). The study is then extended to the case of non-ergodic settings, which enlights a substantial difference between the forward solution process (based on forward Kolmogorov equations) and the backward one. We shall clarify the role that backward solutions play in computing absorption probabilities and in the model- checking of stochastic logics as CSL and CSLTA, which typically require the steady state solution of a non-ergodic CTMC and MRP respectively. Moreover we show that the algorithm for the computation of the whole set of states that satisfy a CSL formula, which is standard practice in CSL model-checkers, can be seen as a case of computation of backward probabilities of Continuous Time Markov Chains (CTMCs). The backward computation of MRP is then inserted in the context of matrix-free solution technique, which allows to deal with MRP of much bigger size than the standard approach based on the computation and solution of the embedded Markov chain.
Sixth International Workshop on Practical Applications of Stochastic Modelling PASM12
Londra
17/9/2012
-
-
-
http://homepages.cs.ncl.ac.uk/nigel.thomas/PASM12.htm
http://www.elsevier.com/journals/electronic-notes-in-theoretical-computer-science/1571-0661
Stochastic Model Checking; Forward and Backward Kolmogorov equations; Markov Renewal Processes
Elvio Gilberto Amparore; Susanna Donatelli
File in questo prodotto:
File Dimensione Formato  
paperPASM.pdf

Accesso riservato

Tipo di file: PREPRINT (PRIMA BOZZA)
Dimensione 1.82 MB
Formato Adobe PDF
1.82 MB Adobe PDF   Visualizza/Apri   Richiedi una copia

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/128236
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? ND
social impact