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

R. Bellman, Dynamic Programming, 1957.

A. Bianco and L. De-alfaro, Model checking of probabilistic and nondeterministic systems, Foundations of Software Technology and Theoretical Computer Science, pp.499-513, 1995.
DOI : 10.1007/3-540-60692-0_70

J. Bogdoll, L. M. Fioriti, A. Hartmanns, and H. Hermanns, Partial Order Methods for Statistical Model Checking and Simulation, Formal Techniques for Distributed Systems, pp.59-74, 2011.
DOI : 10.1145/1755952.1755987

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

H. S. Chang, M. C. Fu, J. Hu, and S. I. Marcus, A survey of some simulation-based algorithms for Markov decision processes, Communications in Information and Systems, vol.7, issue.1, pp.59-92, 2007.
DOI : 10.4310/CIS.2007.v7.n1.a4

E. Clarke, E. A. Emerson, and J. Sifakis, Model checking, Communications of the ACM, vol.52, issue.11, pp.74-84, 2009.
DOI : 10.1145/1592761.1592781

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

H. Hansson and B. Jonsson, A logic for reasoning about time and reliability. Formal aspects of computing, pp.512-535, 1994.

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

W. G. Horner, A New Method of Solving Numerical Equations of All Orders, by Continuous Approximation, Philosophical Transactions of the Royal Society of London, vol.109, issue.0, pp.308-335, 1819.
DOI : 10.1098/rstl.1819.0023

A. Israeli and M. Jalfon, Token management schemes and random walks yield selfstabilizating mutual exclusion, Proc. 9thAnnual ACM Symposium on Principles of Distributed Computing (PODC '90), pp.119-131, 1990.
DOI : 10.1145/93385.93409

C. Jegourel, A. Legay, and S. Sedwards, A platform for high performance statistical model checking ? PLASMA. In Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol.7214, pp.498-503, 2012.
URL : https://hal.archives-ouvertes.fr/hal-01087824

C. Jegourel, A. Legay, and S. Sedwards, Importance Splitting for Statistical Model Checking Rare Properties, Computer Aided Verification, pp.576-591, 2013.
DOI : 10.1007/978-3-642-39799-8_38
URL : https://hal.archives-ouvertes.fr/hal-01087826

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

D. E. Knuth, The Art of Computer Programming, 1998.

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
URL : http://doi.org/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

M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, 1994.
DOI : 10.1002/9780470316887

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

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