www.prismmodelchecker.org
[BKKW17] Christel Baier, Joachim Klein, Sascha Kluppelholz and Sascha Wunderlich. Maximizing the Conditional Expected Reward for Reaching the Goal. In In Proc. 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'17), Springer. 2017. [Introduces novel techniques for computing conditional expected rewards in MDPs, implemented in an extension of PRISM.]
Notes: Available from http://dx.doi.org/10.1007/978-3-662-54580-5_16. Full version at https://arxiv.org/abs/1701.05389. The original publication is available at www.springerlink.com.

Publications