Jasper Berendsen, David N. Jansen, Frits W. Vaandrager. Fortuna: Model Checking Priced Probabilistic Timed Automata. In QEST 2010, Seventh International Conference on the Quantitative Evaluation of Systems, Williamsburg, Virginia, USA, 15-18 September 2010. pages 273-281, IEEE Computer Society, 2010. [doi]