R. Alur and D. L. Dill, A theory of timed automata, Theoretical Computer Science, vol.126, issue.2, pp.183-235, 1994.
DOI : 10.1016/0304-3975(94)90010-8

H. Bohnenkamp, P. D-'argenio, H. Hermanns, and J. P. Katoen, MODEST: A Compositional Modeling Formalism for Hard and Softly Timed Systems, IEEE Transactions on Software Engineering, vol.32, issue.10, pp.812-830, 2006.
DOI : 10.1109/TSE.2006.104

B. Boyer, K. Corre, A. Legay, and S. Sedwards, PLASMA-lab: A Flexible, Distributable Statistical Model Checking Library, pp.160-164, 2013.
DOI : 10.1007/978-3-642-40196-1_12
URL : https://hal.archives-ouvertes.fr/hal-01088411

T. Brázdil, K. Chatterjee, M. Chmelik, V. Forejt, J. Kretínsk´kretínsk´y et al., Verification of Markov Decision Processes Using Learning Algorithms, ATVA. LNCS, pp.98-114, 2014.
DOI : 10.1007/978-3-319-11936-6_8

D. 'argenio, P. Legay, A. Sedwards, S. Traonouez, and L. M. , Smart sampling for lightweight verification of Markov decision processes, STTT, vol.17, issue.4, pp.469-484, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01088633

E. M. Hahn, A. Hartmanns, and H. Hermanns, Reachability and reward checking for stochastic timed automata, ECEASST, vol.70, 2014.

D. Henriques, J. G. Martins, P. Zuliani, A. Platzer, and E. M. Clarke, Statistical Model Checking for Markov Decision Processes, 2012 Ninth International Conference on Quantitative Evaluation of Systems, pp.84-93, 2012.
DOI : 10.1109/QEST.2012.19

T. Hérault, R. Lassaigne, F. Magniette, and S. Peyronnet, Approximate Probabilistic Model Checking, VMCAI. LNCS, pp.73-84, 2004.
DOI : 10.1007/978-3-540-24622-0_8

C. Jégourel, A. Legay, and S. Sedwards, A Platform for High Performance Statistical Model Checking ??? PLASMA, TACAS. LNCS, pp.498-503, 2012.
DOI : 10.1007/978-3-642-28756-5_37

D. E. Knuth, The Art of Computer Programming: Sorting and Searching, 1998.

M. Kwiatkowska, G. Norman, and D. Parker, The PRISM benchmark suite, Proc. 9th International Conference on Quantitative Evaluation of SysTems (QEST'12, pp.203-204, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00740727

M. Z. Kwiatkowska, G. Norman, and D. Parker, Stochastic Games for Verification of Probabilistic Timed Automata, FORMATS. LNCS, pp.212-227, 2009.
DOI : 10.1007/s10703-005-1632-8
URL : https://hal.archives-ouvertes.fr/inria-00457923

M. Z. Kwiatkowska, G. Norman, and D. Parker, PRISM 4.0: Verification of Probabilistic Real-Time Systems, CAV. LNCS, pp.585-591, 2011.
DOI : 10.1007/3-540-45657-0_17
URL : https://hal.archives-ouvertes.fr/hal-00648035

M. Z. Kwiatkowska, G. Norman, D. Parker, and J. Sproston, Performance analysis of probabilistic timed automata using digital clocks, FMSD, vol.29, issue.1, pp.33-78, 2006.

M. Z. Kwiatkowska, G. Norman, R. Segala, and J. Sproston, Automatic verification of real-time systems with discrete probability distributions, Theoretical Computer Science, vol.282, issue.1, pp.101-150, 2002.
DOI : 10.1016/S0304-3975(01)00046-9

M. Z. Kwiatkowska, G. Norman, J. Sproston, and F. Wang, Symbolic model checking for probabilistic timed automata, Information and Computation, vol.205, issue.7, pp.1027-1077, 2007.
DOI : 10.1016/j.ic.2007.01.004

A. Legay, S. Sedwards, and L. Traonouez, Estimating rewards & rare events in nondeterministic systems, ECEASST, vol.72, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01239051

H. L. Younes and R. G. Simmons, Probabilistic Verification of Discrete Event Systems Using Acceptance Sampling, CAV. LNCS, pp.223-235, 2002.
DOI : 10.1007/3-540-45657-0_17