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

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.