Schmalz, Matthias and Varacca, Daniele and Völzer, Hagen  (2009) Counterexamples in Probabilistic LTL Model Checking for Markov Chains.  In: Concur.