R. Alur, C. Courcoubetis, and D. L. Dill, Model-Checking in Dense Real-Time, Information and Computation, vol.104, issue.1, 1993.
DOI : 10.1006/inco.1993.1024
URL : http://doi.org/10.1006/inco.1993.1024

R. Alur and D. L. Dill, A theory of timed automata, Theor. Comput. Sci, 1994.

G. Behrmann, Distributed reachability analysis in timed automata, International Journal on Software Tools for Technology Transfer, vol.11, issue.1, 2005.
DOI : 10.1007/s10009-003-0111-z

G. Behrmann, A. Cougnard, A. David, E. Fleury, K. G. Larsen et al., UPPAAL-Tiga: Time for Playing Games!, Computer Aided Verification, 2007.
DOI : 10.1007/978-3-540-73368-3_14
URL : https://hal.archives-ouvertes.fr/hal-00350466

G. Behrmann, A. David, K. G. Larsen, P. Pettersson, and W. Yi, Developing UPPAAL over 15 years, Software: Practice and Experience, vol.292, issue.6, 2011.
DOI : 10.1002/spe.1006

G. Behrmann, A. David, K. G. Larsen, and W. Yi, Unification & sharing in timed automata verification, SPIN, 2003.

G. Behrmann, A. Fehnker, T. Hune, K. G. Larsen, P. Pettersson et al., Efficient Guiding Towards Cost-Optimality in UPPAAL, TACAS, number 2031 in LNCS, 2001.
DOI : 10.7146/brics.v8i4.20458

G. Behrmann, A. Fehnker, T. Hune, K. G. Larsen, P. Pettersson et al., Minimum-Cost Reachability for Priced Timed Automata, HSCC, number 2034 in LNCS, 2001.
DOI : 10.7146/brics.v8i3.20457
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.164.8691

G. Behrmann, T. Hune, and F. Vaandrager, Distributed timed model checking - How the search order matters, CAV, 2000.
DOI : 10.1007/10722167_19
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.36.5438

G. Behrmann, K. G. Larsen, J. Pearson, C. Weise, and W. Yi, Efficient timed reachability analysis using clock difference d iagrams, CAV, 1999.
DOI : 10.7146/brics.v5i47.19492
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.16.4832

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

P. E. Bulychev, A. David, K. G. Larsen, A. Legay, and M. Mikucionis, Computing Nash Equilibrium in Wireless Ad Hoc Networks: A Simulation-Based Approach, IWIGP, 2012.
DOI : 10.4204/EPTCS.78.1

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), 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, P. G. Jensen, K. G. Larsen, A. Legay, D. Lime et al., On Time with Minimal Expected Cost!, 2014.
DOI : 10.1007/978-3-319-11936-6_10

A. David, P. G. Jensen, K. G. Larsen, M. Mikucionis, and J. H. Taankvist, Uppaal stratego In Tools and Algorithms for the Construction and Analysis of Systems, 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software Proceedings, 2015.

A. David, K. G. Larsen, A. Legay, M. Mikucionis, D. B. Poulsen et al., Runtime Verification of Biological Systems, Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change -5th International Symposium Proceedings, Part I, 2012.
DOI : 10.1007/978-3-642-34026-0_29
URL : https://hal.archives-ouvertes.fr/hal-01088165

A. David, K. G. Larsen, A. Legay, M. Mikucionis, D. B. Poulsen et al., Statistical model checking for biological systems, International Journal on Software Tools for Technology Transfer, vol.13, issue.11, 2015.
DOI : 10.1007/s10009-014-0323-4

A. David, K. G. Larsen, A. Legay, M. Mikucionis, and Z. Wang, Time for Statistical Model Checking of Real-Time Systems, In CAV LNCS, vol.8, issue.3, 2011.
DOI : 10.1007/s10009-005-0187-8

A. David, M. O. Möller, and W. Yi, Formal Verification of UML Statecharts with Real-Time Extensions, Fundamental Approaches to Software Engineering, 5th International Conference, 2002.
DOI : 10.1007/3-540-45923-5_15

D. Helbing and P. Molnár, Social force model for pedestrian dynamics, Physical Review E, vol.51, issue.5, 1995.
DOI : 10.1103/PhysRevE.51.4282
URL : http://arxiv.org/abs/cond-mat/9805244

M. Hendriks and K. G. Larsen, Exact Acceleration of Real-Time Model Checking, Electronic Notes in Theoretical Computer Science, vol.65, issue.6, 2002.
DOI : 10.1016/S1571-0661(04)80473-0
URL : http://doi.org/10.1016/s1571-0661(04)80473-0

T. A. Henzinger and P. Ho, Algorithmic analysis of nonlinear hybrid systems, CAV
DOI : 10.1109/9.664156
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.472.2783

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

C. Jegourel, A. Legay, and S. Sedwards, A Platform for High Performance Statistical Model Checking ??? PLASMA, TACAS, 2012.
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, CAV, 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, 2013.
DOI : 10.1007/978-3-642-39799-8_38
URL : https://hal.archives-ouvertes.fr/hal-01087826

C. Jégourel, A. Legay, S. Sedwards, and L. Traonouez, Distributed verification of rare properties using importance splitting observers, ECEASST, 2015.

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, 1953.
DOI : 10.1287/opre.1.5.263

K. G. Larsen, G. Behrmann, E. Brinksma, A. Fehnker, T. Hune et al., As Cheap as Possible: Effcient Cost-Optimal Reachability for Priced Timed Automata, CAV, number 2102 in LNCS, 2001.
DOI : 10.1007/3-540-44585-4_47

K. G. Larsen, P. Pettersson, and W. Yi, Uppaal in a nutshell, International Journal on Software Tools for Technology Transfer, vol.1, issue.1-2, 1997.
DOI : 10.1007/s100090050010

K. G. Larsen and A. Skou, Bisimulation through probabilistic testing, Information and Computation, vol.94, issue.1, 1991.
DOI : 10.1016/0890-5401(91)90030-6
URL : http://doi.org/10.1016/0890-5401(91)90030-6

F. Larsson, K. G. Larsen, P. Pettersson, and W. Yi, Efficient verification of realtime systems: Compact data structures and state-space reduction, Proc. of the 18th IEEE Real-Time Systems Symposium, 1997.

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

K. Sen, M. Viswanathan, and G. Agha, Statistical Model Checking of Black-Box Probabilistic Systems, CAV, LNCS 3114, 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, 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), 2005.
DOI : 10.1109/QEST.2005.42

A. Wald, Sequential tests of statistical hypotheses, Annals of Mathematical Statistics, 1945.

E. R. Wognsen, B. R. Haverkort, M. R. Jongerden, R. R. Hansen, and K. G. Larsen, A Score Function for Optimizing the Cycle-Life of Battery-Powered Embedded Systems, Formal Modeling and Analysis of Timed Systems -13th International Conference Proceedings, 2015.
DOI : 10.1007/978-3-319-22975-1_20

W. Yi, P. Pettersson, and M. Daniels, Automatic Verification of Real-Time Communicating Systems by Constraint-Solving, Proceedings of the 7th IFIP WG6
DOI : 10.1007/978-0-387-34878-0_18

H. L. Younes, Verification and Planning for Stochastic Processes with Asynchronous Events, 2005.

P. Zuliani, A. Platzer, and E. M. Clarke, Bayesian statistical model checking with application to Stateflow/Simulink verification. Formal Methods in System Design, 2013.
DOI : 10.1007/s10703-013-0195-3
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.188.3451