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