R. Alur, C. Courcoubetis, and D. L. Dill, Verifying automata specifications of probabilistic real-time systems, Proc. REX Workshop on Real-Time: Theory in Practice, pp.28-44, 1992.
DOI : 10.1007/BFb0031986

R. Alur and D. L. Dill, Automata for modeling real-time systems, Proc. 17th International Colloquium on Automata, Languages and Programming (ICALP'90), pp.322-335, 1990.
DOI : 10.1007/BFb0032042

R. Alur and D. L. Dill, [AL02] Luca Aceto and François Laroussinie Is your model-checker on time? On the complexity of model-checking for timed modal logics Optimal paths in weighted timed automata, Proc. 4th International Workshop on Hybrid Systems: Computation and Control (HSCC'01), volume 2034 of Lecture Notes in Computer Science, pp.183-235, 1994.

E. Asarin, O. Maler, A. Pnueli, and J. Sifakis, Controller synthesis for timed automata, Proc. IFAC Symposium on System Structure and Control, pp.469-474, 1998.

A. Aziz, K. Sanwal, V. Singhal, and R. K. Brayton, Model-checking continuous-time Markov chains, ACM Transactions on Computational Logic, vol.1, issue.1, pp.162-170, 2000.
DOI : 10.1145/343369.343402
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.18.8774

C. Baier, N. Bertrand, P. Bouyer, T. Brihaye, and M. Größer, Probabilistic and Topological Semantics for Timed Automata, Proc. 27th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'07), pp.179-191, 2007.
DOI : 10.1007/978-3-540-77050-3_15
URL : https://hal.archives-ouvertes.fr/inria-00424526

N. Bertrand, P. Bouyer, T. Brihaye, N. Bouyer, T. Brihaye et al., Quantitative modelchecking of one-clock timed automata under probabilistic semantics Almost-sure modelchecking of reactive timed automata Locks: Picking key methods for a scalable quantitative analysis, Proc. 5th International Conference on Quantitative Evaluation of Systems Proc. 9th International Conference on Quantitative Evaluation of Systems (QEST'12) Proc. 3rd International Conference on Quantitative Evaluation of Systems (QEST'06), pp.138-147258, 2006.

M. Bozga, C. Daws, O. Maler, A. Olivero, S. Tripakis et al., Kronos: A model-checking tool for real-time systems, Proc. 10th International Conference on Computer Aided Verification (CAV'98), pp.546-550, 1998.
DOI : 10.1007/BFb0028779
URL : https://hal.archives-ouvertes.fr/hal-00374788

P. Bouyer, V. Forejt-gerd-behrmann, A. Fehnker, T. Hune, K. G. Larsen et al., Reachability in Stochastic Timed Games, Proc. 36th International Colloquium on Automata, Languages and Programming Proc. 4th International Workshop on Hybrid Systems: Computation and Control (HSCC'01), volume 2034 of Lecture Notes in Computer Science, pp.103-114, 2001.
DOI : 10.1007/978-3-642-02930-1_9

P. Bouyer, U. Fahrenberg, K. G. Larsen, and N. Markey, Quantitative analysis of real-time systems using priced timed automata, Communications of the ACM, vol.54, issue.9, pp.78-87, 2011.
DOI : 10.1145/1995376.1995396
URL : https://hal.archives-ouvertes.fr/hal-01088030

C. Baier, B. 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

P. Billingsley, Probability and measure. Wiley Series in Probability and Mathematical Statistics, 1995.

C. Baier and M. Z. Kwiatkowska, On the verification of qualitative properties of probabilistic processes under fairness constraints, Information Processing Letters, vol.66, issue.2, pp.71-79, 1998.
DOI : 10.1016/S0020-0190(98)00038-6

N. Bertrand and S. Schewe, Playing Optimally on Timed Automata with Random Delays, Proc. 10th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS'12), pp.43-58, 2012.
DOI : 10.1007/978-3-642-33365-1_5
URL : https://hal.archives-ouvertes.fr/hal-00752440

H. C. Bohnenkamp, H. Peter-van-der-stok, F. W. Hermanns, and . Vaandrager, Costoptimization of the IPv4 Zeroconf protocol, Proc. International Conference on Dependable Systems and Networks (DSN'03), pp.531-540, 2003.

T. Chen, T. Han, J. Katoen, and A. Mereacre, Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications, Logical Methods in Computer Science, vol.7, issue.1, pp.1-34, 2011.
DOI : 10.2168/LMCS-7(1:12)2011

F. Cassez, T. A. Henzinger, and J. Raskin, A Comparison of Control Problems for Timed and Hybrid Systems, Proc. 5th International Workshop on Hybrid Systems: Computation and Control, pp.134-148, 2002.
DOI : 10.1007/3-540-45873-5_13

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

E. Chang, Z. Manna, and A. Pnueli, Characterization of temporal property classes, Proc. 19th Int. Coll. Automata, Languages, and Programming (ICALP'92), pp.474-486, 1992.
DOI : 10.1007/3-540-55719-9_97

L. Martin-de-wulf, J. Doyen, and . Raskin, Almost ASAP Semantics: From Timed Models to Timed Implementations, Proc. 7th International Workshop on Hybrid Systems: Computation and Control, pp.296-310, 2004.
DOI : 10.1007/978-3-540-24743-2_20

S. Donatelli, S. Haddad, and J. Sproston, Model Checking Timed and Stochastic Properties with CSL^{TA}, IEEE Transactions on Software Engineering, vol.35, issue.2, pp.224-240, 2009.
DOI : 10.1109/TSE.2008.108
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.217.6677

J. Desharnais and P. Panangaden, Continuous stochastic logic characterizes bisimulation of continuous-time Markov processes, Thomas A. Henzinger, and Radha Jagadeesan. Robust timed automata Proc. International Workshop on Hybrid and Real-Time Systems (HART'97), volume 1201 of Lecture Notes in Computer Science, pp.99-115, 1997.
DOI : 10.1016/S1567-8326(02)00068-1

M. Kwiatkowska, G. Norman, and D. Parker, PRISM 4.0: Verification of Probabilistic Real-Time Systems, Proc. 23rd International Conference on Computer Aided Verification (CAV'11), pp.585-591, 2011.
DOI : 10.1007/3-540-45657-0_17
URL : https://hal.archives-ouvertes.fr/hal-00648035

M. Z. Kwiatkowska, G. Norman, R. Segala, and J. Sproston, Verifying Quantitative Properties of Continuous Probabilistic Timed Automata, Proc. 11th International Conference on Concurrency Theory, pp.123-137, 2000.
DOI : 10.1007/3-540-44618-4_11

M. Z. Kwiatkowska, G. Norman, R. Segala, and J. Sproston, Automatic verification of real-time systems with discrete probability distributions, Theoretical Computer Science, vol.282, issue.1, pp.101-150, 2002.
DOI : 10.1016/S0304-3975(01)00046-9

J. G. Kemeny, J. L. Snell, and A. W. Knapp, François Laroussinie, Nicolas Markey, and Philippe Schnoebelen. Model checking timed automata with one or two clocks, Proc. 15th International Conference on Concurrency Theory, pp.387-401, 1976.

N. Markey, Robustness in real-time systems, 2011 6th IEEE International Symposium on Industrial and Embedded Systems, pp.28-34, 2011.
DOI : 10.1109/SIES.2011.5953652

C. John and . Oxtoby, The Banach-Mazur game and Banach category theorem, Contributions to the Theory of Games, pp.159-163, 1957.

A. Pnueli, The temporal logic of programs, 18th Annual Symposium on Foundations of Computer Science (sfcs 1977), pp.46-57, 1977.
DOI : 10.1109/SFCS.1977.32

A. Pnueli, On the extremely fair treatment of probabilistic algorithms, Proceedings of the fifteenth annual ACM symposium on Theory of computing , STOC '83, pp.278-290, 1983.
DOI : 10.1145/800061.808757

A. Pnueli and L. D. Zuck, Probabilistic verification. Information and Computation, pp.1-29, 1993.

O. Sankur, T. Robustness-in, and . Automata, Analysis, Synthesis, Implementation [SBM11] Ocan Sankur, Patricia Bouyer, and Nicolas Markey. Shrinking timed automata, Proc. 31st Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'11), volume 13 of Leibniz International Proceedings in Informatics Leibniz-Zentrum für Informatik, pp.90-102, 2011.

M. Stoelinga, Fun with FireWire: A Comparative Study of Formal Verification Methods Applied to the IEEE 1394 Root Contention Protocol, Formal Aspects of Computing, vol.14, issue.3, pp.328-337, 2003.
DOI : 10.1007/s001650300009

M. Y. Vardi, Automatic verification of probabilistic concurrent finite state programs, 26th Annual Symposium on Foundations of Computer Science (sfcs 1985), pp.327-338, 1985.
DOI : 10.1109/SFCS.1985.12

D. Varacca and H. Völzer, Temporal Logics and Model Checking for Fairly Correct Systems, 21st Annual IEEE Symposium on Logic in Computer Science (LICS'06), pp.389-398, 2006.
DOI : 10.1109/LICS.2006.49
URL : https://hal.archives-ouvertes.fr/hal-00148934

Y. Moshe, P. Vardi, [. Wolper, D. N. Zhang, F. Jansen et al., Reasoning about infinite computations Information and Computation Automata-based CSL model checking, Proc. 38th International Colloquium on Automata, Languages and Programming (ICALP'11), pp.1-37, 1994.