Computing Expected Hitting Times for Imprecise Markov Chains

We present a novel algorithm to solve a non-linear system of equations, whose solution can be interpreted as a tight lower bound on the vector of expected hitting times of a Markov chain whose transition probabilities are only partially specified. We also briefly sketch how this method can be modified to solve a conjugate system of equations that gives rise to the corresponding upper bound. We prove the correctness of our method and show that it converges to the correct solution in a finite number of steps under mild conditions on the system. We compare the runtime complexity of our method to a previously published method from the literature and identify conditions under which our novel method is more efficient.