C. Baier, B. R. Haverkort, H. Hermanns, and J. Katoen, Model-checking algorithms for continuous-time markov chains, IEEE Transactions on Software Engineering, vol.29, issue.6, pp.524-541, 2003.
DOI : 10.1109/TSE.2003.1205180

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

F. Ciesinski and M. Größer, On Probabilistic Computation Tree Logic, Validation of Stochastic Systems, pp.147-188, 2004.
DOI : 10.1007/978-3-540-24611-4_5

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

A. Colombo, D. Fontanelli, D. Gandhi, A. De-angeli, L. Palopoli et al., Behavioural templates improve robot motion planning with social force model in human environments, 2013 IEEE 18th Conference on Emerging Technologies & Factory Automation (ETFA), pp.1-6, 2013.
DOI : 10.1109/ETFA.2013.6648081
URL : https://hal.archives-ouvertes.fr/hal-01088063

A. Colombo, D. Fontanelli, A. Legay, L. Palopoli, and S. Sedwards, Motion planning in crowds using statistical model checking to enhance the social force model, 52nd IEEE Conference on Decision and Control, 2013.
DOI : 10.1109/CDC.2013.6760437
URL : https://hal.archives-ouvertes.fr/hal-01088031

A. David, D. Du, K. G. Larsen, A. Legay, M. Miku?ionis et al., Statistical Model Checking for Stochastic Hybrid Systems, Proceedings First International Workshop on Hybrid Systems and Biology of Electronic Proceedings in Theoretical Computer Science, pp.122-136, 2012.
DOI : 10.4204/EPTCS.92.9
URL : https://hal.archives-ouvertes.fr/hal-01088197

A. David, K. G. Larsen, A. Legay, M. Miku?ionis, D. B. Poulsen et al., Runtime Verification of Biological Systems, Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change, pp.388-404, 2012.
DOI : 10.1007/978-3-642-34026-0_29
URL : https://hal.archives-ouvertes.fr/hal-01088165

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. Helbing and P. Molnár, Social force model for pedestrian dynamics, Physical Review E, vol.51, issue.5, pp.4282-4286, 1995.
DOI : 10.1103/PhysRevE.51.4282

D. Henriques, J. G. Martins, P. Zuliani, A. Platzer, E. M. Clarke et al., Statistical model checking for Markov decision processes Approximate probabilistic model checking, Quantitative Evaluation of Systems Ninth International Conference on VMCAI, volume 2937 of LNCS, pp.84-93, 2004.

C. Jegourel, A. Legay, and S. Sedwards, A Platform for High Performance Statistical Model Checking ??? PLASMA
DOI : 10.1007/978-3-642-28756-5_37
URL : https://hal.archives-ouvertes.fr/hal-01087824

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

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

H. Kahn and A. W. Marshall, Methods of Reducing Sample Size in Monte Carlo Computations, Journal of the Operations Research Society of America, vol.1, issue.5, pp.263-278, 1953.
DOI : 10.1287/opre.1.5.263

M. Z. Kwiatkowska, G. Norman, and J. Sproston, Probabilistic Model Checking of the IEEE 802.11 Wireless Local Area Network Protocol, Proceedings of the Second 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 and S. Sedwards, Lightweight Monte Carlo verification of Markov decision processes, 2014.

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, 1959.
DOI : 10.1007/BF02883985

A. Pnueli and L. Zuck, Verification of multiprocess probabilistic protocols, Distributed Computing, vol.17, issue.1, pp.53-72, 1986.
DOI : 10.1007/BF01843570

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

A. Ridder, Importance Sampling Simulations of Markovian Reliability Systems Using Cross-Entropy, Annals of Operations Research, vol.40, issue.7, pp.119-136, 2005.
DOI : 10.1007/s10479-005-5727-9

K. Sen, M. Viswanathan, and G. Agha, Statistical Model Checking of Black-Box Probabilistic Systems, CAV, pp.202-215, 2004.
DOI : 10.1007/978-3-540-27813-9_16

K. Sen, M. Viswanathan, and G. Agha, On Statistical Model Checking of Stochastic Systems, CAV, pp.266-280, 2005.
DOI : 10.1007/11513988_26

K. Sen, M. Viswanathan, and G. A. Agha, VESTA: A statistical model-checker and analyzer for probabilistic systems, Second International Conference on the Quantitative Evaluation of Systems (QEST'05), pp.251-252, 2005.
DOI : 10.1109/QEST.2005.42

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.