P. Buchholz, J. Kriege, and D. Scheftelowitsch, “Equivalence and Minimization for Model Checking Labeled Markov Chains”, EAI Endorsed Scal Inf Syst, vol. 3, no. 11, p. e2, Jan. 2016.