R. Alur, C. Courcoubetis, N. Halbwachs, T. A. Henzinger, P. Ho et al., The algorithmic analysis of hybrid systems, Theoretical Computer Science, vol.138, issue.1, pp.3-34, 1995.
DOI : 10.1016/0304-3975(94)00202-T

R. Alur and D. L. Dill, A theory of timed automata, Theoretical Computer Science, vol.126, issue.2, pp.183-235, 1994.
DOI : 10.1016/0304-3975(94)90010-8

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

G. Bacci, G. Bacci, K. G. Larsen, and R. Mardare, On-the-Fly Exact Computation of Bisimilarity Distances, TACAS, pp.1-15, 2013.
DOI : 10.1007/978-3-642-36742-7_1

S. S. Bauer, U. Fahrenberg, L. Juhl, K. G. Larsen, A. Legay et al., Weighted modal transition systems, Formal Methods in System Design, vol.806, issue.1, 2013.
DOI : 10.1007/s10703-012-0178-9
URL : https://hal.archives-ouvertes.fr/hal-01087925

S. S. Bauer, U. Fahrenberg, A. Legay, and C. Thrane, General Quantitative Specification Theories with Modalities, pp.18-30, 2012.
DOI : 10.1007/978-3-642-30642-6_3
URL : https://hal.archives-ouvertes.fr/hal-01087983

U. Boker and T. A. Henzinger, Approximate determinization of quantitative automata, FSTTCS, pp.362-373, 2012.

P. Bouyer, K. G. Larsen, N. Markey, O. Sankur, and C. Thrane, Timed Automata Can Always Be Made Implementable, In CONCUR, vol.79, issue.7, pp.76-91, 2011.
DOI : 10.1016/j.jlap.2010.07.010
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.396.9857

P. ?erný, T. A. Henzinger, and A. Radhakrishna, Simulation distances, pp.253-268, 2010.

P. ?erný, T. A. Henzinger, and A. Radhakrishna, Quantitative abstraction refinement, POPL, pp.115-128, 2013.

K. Chatterjee, L. De-alfaro, M. Faella, T. A. Henzinger, R. Majumdar et al., Compositional quantitative reasoning, QEST, pp.179-188, 2006.

K. Chatterjee, L. Doyen, and T. A. Henzinger, Quantitative languages, ACM Trans. Comput. Log, vol.11, issue.4, 2010.
DOI : 10.1145/1805950.1805953
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.158.9296

L. De-alfaro, M. Faella, T. A. Henzinger, R. Majumdar, and M. Stoelinga, Model checking discounted temporal properties, Theoretical Computer Science, vol.345, issue.1, pp.139-170, 2005.
DOI : 10.1016/j.tcs.2005.07.033

L. De-alfaro, M. Faella, and M. Stoelinga, Linear and Branching Metrics for Quantitative Transition Systems, ICALP, pp.97-109, 2004.
DOI : 10.1007/978-3-540-27836-8_11

L. De-alfaro, M. Faella, and M. Stoelinga, Linear and Branching System Metrics, IEEE Transactions on Software Engineering, vol.35, issue.2, pp.258-273, 2009.
DOI : 10.1109/TSE.2008.106

J. Desharnais, V. Gupta, R. Jagadeesan, and P. Panangaden, Metrics for labelled Markov processes, Theoretical Computer Science, vol.318, issue.3, pp.323-354, 2004.
DOI : 10.1016/j.tcs.2003.09.013

M. Droste and P. Gastin, Weighted automata and weighted logics, Theoretical Computer Science, vol.380, issue.1-2, pp.69-86, 2007.
DOI : 10.1016/j.tcs.2007.02.055
URL : https://hal.archives-ouvertes.fr/hal-00772642

M. Droste and I. Meinecke, Weighted automata and weighted MSO logics for average and long-time behaviors, Information and Computation, vol.220, issue.221, pp.44-59, 2012.
DOI : 10.1016/j.ic.2012.10.001

M. Droste and G. Rahonis, Weighted automata and weighted logics with discounting, TCS, issue.37, pp.4103481-3494, 2009.

A. Ehrenfeucht and J. Mycielski, Positional strategies for mean payoff games, International Journal of Game Theory, vol.59, issue.2, pp.109-113, 1979.
DOI : 10.1007/BF01768705

U. Fahrenberg, A. Legay, and C. Thrane, The quantitative linear-time?branchingtime spectrum, FSTTCS, pp.103-114, 2011.

G. Frehse, C. L. Guernic, A. Donzé, S. Cotton, R. Ray et al., SpaceEx: Scalable Verification of Hybrid Systems, CAV, pp.379-395, 2011.
DOI : 10.1007/978-3-642-00768-2_32
URL : https://hal.archives-ouvertes.fr/hal-00769608

S. Gilmore and J. Hillston, The PEPA workbench: A tool to support a process algebra-based approach to performance modelling, CPE, pp.353-368, 1994.
DOI : 10.1007/3-540-58021-2_20

A. Girard, Synthesis using approximately bisimilar abstractions: time-optimal control problems, 49th IEEE Conference on Decision and Control (CDC), pp.5893-5898, 2010.
DOI : 10.1109/CDC.2010.5717756
URL : https://hal.archives-ouvertes.fr/hal-00769592

A. Girard and G. J. Pappas, Approximation Metrics for Discrete and Continuous Systems, IEEE Transactions on Automatic Control, vol.52, issue.5, pp.782-798, 2007.
DOI : 10.1109/TAC.2007.895849
URL : https://hal.archives-ouvertes.fr/hal-00171714

H. Hansson and B. Jonsson, A logic for reasoning about time and reliability, Formal Aspects of Computing, vol.2, issue.1, pp.512-535, 1994.
DOI : 10.1007/BF01211866

T. A. Henzinger, P. Ho, and H. Wong-toi, HYTECH: a??model checker for hybrid systems, International Journal on Software Tools for Technology Transfer, vol.1, issue.1-2, pp.110-122, 1997.
DOI : 10.1007/s100090050008

T. A. Henzinger, R. Majumdar, and V. S. Prabhu, Quantifying Similarities Between Timed Systems, FORMATS, pp.226-241, 2005.
DOI : 10.1007/11603009_18
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.212.6464

T. A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine, Symbolic model checking for real-time systems, [1992] Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science, pp.193-244, 1994.
DOI : 10.1109/LICS.1992.185551
URL : http://doi.org/10.1006/inco.1994.1045

J. Hillston, A Compositional Approach to Performance Modelling, 1996.
DOI : 10.1017/CBO9780511569951

R. Koymans, Specifying real-time properties with metric temporal logic. Real-Time Systems, pp.255-299, 1990.
DOI : 10.1007/bf01995674

M. Z. Kwiatkowska, G. Norman, and D. Parker, Probabilistic symbolic model checking with PRISM: A hybrid approach, TACAS, pp.52-66, 2002.
DOI : 10.1007/3-540-46002-0_5
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.10.5908

K. G. Larsen, A. Legay, L. Traonouez, and A. W?sowski, Robust Specification of Real Time Components, FORMATS, pp.129-144, 2011.
DOI : 10.1007/s00165-005-0067-8
URL : https://hal.archives-ouvertes.fr/hal-01088002

K. G. Larsen, R. Mardare, and P. Panangaden, Taking It to the Limit: Approximate Reasoning for Markov Processes, MFCS, pp.681-692, 2012.
DOI : 10.1007/978-3-642-32589-2_59

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, pp.134-152, 1997.
DOI : 10.1007/s100090050010

F. W. Lawvere, Metric spaces, generalized logic, and closed categories. Rendiconti del seminario matématico e fisico di, pp.135-166, 1973.
DOI : 10.1007/bf02924844

P. Panangaden, Labelled Markov Processes, 2009.
DOI : 10.1142/p595

J. Quesel, M. Fränzle, and W. Damm, Crossing the Bridge between Similar Games, FORMATS, pp.160-176, 2011.
DOI : 10.1007/s00165-005-0067-8

R. Segala and N. A. Lynch, Probabilistic simulations for probabilistic processes, CONCUR, pp.481-496, 1994.

W. J. Stewart, Introduction to the Numerical Solution of Markov Chains, 1994.

C. Stirling, Modal and temporal logics for processes, Banff Higher Order Workshop, pp.149-237, 1995.
DOI : 10.1007/3-540-60915-6_5
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.36.9078

C. Thrane, U. Fahrenberg, and K. G. Larsen, Quantitative analysis of weighted transition systems, The Journal of Logic and Algebraic Programming, vol.79, issue.7, pp.689-703, 2010.
DOI : 10.1016/j.jlap.2010.07.010

F. Van-breugel, An introduction to metric semantics: operational and denotational models for programming and specification languages, Theoretical Computer Science, vol.258, issue.1-2, pp.1-98, 2001.
DOI : 10.1016/S0304-3975(00)00403-5

F. Van-breugel and J. Worrell, A behavioural pseudometric for probabilistic transition systems, Theoretical Computer Science, vol.331, issue.1, pp.115-142, 2005.
DOI : 10.1016/j.tcs.2004.09.035

F. Van-breugel and J. Worrell, Approximating and computing behavioural distances in probabilistic transition systems, Theoretical Computer Science, vol.360, issue.1-3, pp.373-385, 2006.
DOI : 10.1016/j.tcs.2006.05.021

F. Wang, A. K. Mok, and E. A. Emerson, Symbolic model checking for distributed real-time systems, FME, pp.632-651, 1993.
DOI : 10.1007/BFb0024671

G. Zheng and A. Girard, Bounded and Unbounded Safety Verification Using Bisimulation Metrics, HSCC, pp.426-440, 2009.
DOI : 10.1007/978-3-540-71493-4_46
URL : https://hal.archives-ouvertes.fr/hal-00379746

U. Zwick and M. Paterson, The complexity of mean payoff games, COCOON, pp.1-10, 1995.
DOI : 10.1007/BFb0030814