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 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.

B. Boyer, K. Corre, A. Legay, and S. Sedwards, PLASMAlab: A flexible, distributable statistical model checking library, Quantitative Evaluation of Systems, pp.160-164, 2013.
URL : https://hal.archives-ouvertes.fr/hal-01088411

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

E. M. 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

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

C. Eisner, D. Fisman, J. Havlicek, Y. Lustig, A. Mcisaac et al., Reasoning with Temporal Logic on Truncated Paths, Computer Aided Verification, pp.27-39, 2003.
DOI : 10.1007/978-3-540-45069-6_3

M. C. Geilen, On the Construction of Monitors for Temporal Logic Properties, Electronic Notes in Theoretical Computer Science, vol.55, issue.2, pp.181-199, 2001.
DOI : 10.1016/S1571-0661(04)00252-X

R. Gerth, D. Peled, M. Y. Vardi, P. Vardi, and . Wolper, Simple On-the-fly Automatic Verification of Linear Temporal Logic, Protocol Specification Testing and Verification, pp.3-18, 1995.
DOI : 10.1007/978-0-387-34892-6_1

D. Giannakopoulou and K. Havelund, Automata-based verification of temporal properties on running programs, Proceedings 16th Annual International Conference on Automated Software Engineering (ASE 2001), pp.412-416, 2001.
DOI : 10.1109/ASE.2001.989841

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. 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 self-stabilizating mutual exclusion, Proc. 9th Annual ACM Symposium on Principles of Distributed Computing (PODC '90), pp.119-131, 1990.

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.

E. Donald and . 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 J. Sproston, Performance analysis of probabilistic timed automata using digital clocks, Formal Methods in System Design, vol.29, issue.1, pp.33-78, 2006.
DOI : 10.1007/s10703-006-0005-2

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

M. Z. Kwiatkowska, G. Norman, and J. Sproston, Probabilistic Model Checking of the IEEE 802.11 Wireless Local Area Network Protocol, Proc. 2 nd Joint International Workshop on Process Algebra and Probabilistic Methods, Performance Modeling and Verification, pp.169-187, 2002.
DOI : 10.1007/3-540-45605-8_11

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, 4th 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

Z. Manna and A. Pnueli, Temporal Verification of Reactive Systems: Safety, 1995.
DOI : 10.1007/978-1-4612-4222-2

U. Ndukwu and A. Mciver, An expectation transformer approach to predicate abstraction and data independence for probabilistic programs, Proc. 8th 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.

A. Wald, Sequential Tests of Statistical Hypotheses, The Annals of Mathematical Statistics, vol.16, issue.2, pp.117-186, 1945.
DOI : 10.1214/aoms/1177731118

D. J. White, Real Applications of Markov Decision Processes, Interfaces, vol.15, issue.6, pp.73-83, 1985.
DOI : 10.1287/inte.15.6.73

D. J. White, Further Real Applications of Markov Decision Processes, Interfaces, vol.18, issue.5, pp.55-61, 1988.
DOI : 10.1287/inte.18.5.55

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, Verification and Planning for Stochastic Processes with Asynchronous Events, 2005.

L. S. Håkan, R. G. Younes, and . Simmons, Probabilistic verification of discrete event systems using acceptance sampling, Computer Aided Verification, pp.223-235, 2002.