C. Baier and J. Katoen, Principles of model checking, 2008.

J. Bogdoll and L. Fioriti, Arnd Hartmanns, and Holger Hermanns . Partial order methods for statistical model checking and simulation, Formal Techniques for Distributed Systems, pp.59-74, 2011.

T. Brázdil, K. Chatterjee, M. Chmelík, M. Vojt?ch-forejt-k?etínsk´k?etínsk´y, D. Kwiatkowska et al., Verification of Markov Decision Processes Using Learning Algorithms, Automated Technology for Verification and Analysis, pp.98-114, 2014.
DOI : 10.1007/978-3-319-11936-6_8

H. Thomas, C. E. Cormen, R. L. Leiserson, C. Rivest, and . Stein, Introduction to Algorithms, 2009.

D. Pedro, A. Argenio, S. Legay, L. Sedwards, and . Traonouez, Smart sampling for lightweight verification of Markov decision processes, International Journal on Software Tools for Technology Transfer, vol.17, issue.4, pp.469-484, 2015.

A. Hartmanns and M. Timmer, On-the-Fly Confluence Detection for Statistical Model Checking, NASA Formal Methods, pp.337-351, 2013.
DOI : 10.1007/978-3-642-38088-4_23

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

W. Hoeffding, Probability Inequalities for Sums of Bounded Random Variables, Journal of the American Statistical Association, vol.1, issue.301, pp.13-30, 1963.
DOI : 10.1214/aoms/1177730491

C. Jegourel, A. Legay, and S. Sedwards, Cross-Entropy Optimisation of Importance Sampling Parameters for Statistical Model Checking, Computer Aided Verification, pp.327-342, 2012.
DOI : 10.1007/978-3-642-31424-7_26
URL : https://hal.archives-ouvertes.fr/hal-01087341

M. Kearns, Y. Mansour, and A. Y. Ng, A sparse sampling algorithm for near-optimal planning in large Markov decision processes, Machine Learning, pp.193-208, 2002.

M. Kwiatkowska, G. Norman, and D. Parker, Stochastic Model Checking, Formal Methods for the Design of Computer, Communication and Software Systems: Performance Evaluation (SFM'07), pp.220-270, 2007.
DOI : 10.1007/978-3-540-72522-0_6

M. Kwiatkowska, G. Norman, and D. Parker, Analysis of a gossip protocol in PRISM, ACM SIGMETRICS Performance Evaluation Review, vol.36, issue.3, pp.17-22, 2008.
DOI : 10.1145/1481506.1481511

M. Kwiatkowska, G. Norman, D. Parker, and M. G. Vigliotti, Probabilistic Mobile Ambients, Theoretical Computer Science, vol.410, issue.12-13, pp.12-131272, 2009.
DOI : 10.1016/j.tcs.2008.12.058

R. Lassaigne and S. Peyronnet, Approximate planning and verification for large markov decision processes, Proceedings of the 27th Annual ACM Symposium on Applied Computing, SAC '12, pp.1314-1319, 2012.
DOI : 10.1145/2245276.2231984
URL : https://hal.archives-ouvertes.fr/hal-01149843

A. Legay, S. Sedwards, and L. Traonouez, Scalable Verification of Markov Decision Processes, 4 th Workshop on Formal Methods in the Development of Software (FMDS 2014), 2014.
DOI : 10.1007/978-3-319-15201-1_23
URL : https://hal.archives-ouvertes.fr/hal-01088396

U. Ndukwu and A. Mciver, An expectation transformer approach to predicate abstraction and data independence for probabilistic programs, Proc. 8 th Workshop on Quantitative Aspects of Programming Languages, 2010.
DOI : 10.4204/EPTCS.28.9

M. Okamoto, Some inequalities relating to the partial sum of binomial probabilities, Annals of the Institute of Statistical Mathematics, vol.7, issue.1, pp.29-35, 1958.
DOI : 10.1007/BF02883985

L. Martin and . Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, 1994.

P. Shahabuddin, Importance Sampling for the Simulation of Highly Reliable Markovian Systems, Management Science, vol.40, issue.3, pp.333-352, 1994.
DOI : 10.1287/mnsc.40.3.333

D. J. White, A Survey of Applications of Markov Decision Processes, Journal of the Operational Research Society, vol.44, issue.11, pp.1073-1096, 1993.
DOI : 10.1057/jors.1993.181