D. Charalambos, K. C. Aliprantis, and . Border, Infinite Dimensional Analysis: A Hitchhiker's Guide, 2007.

R. Alur and D. 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

S. Sebastian, A. Bauer, R. David, K. G. Hennicker, A. Larsen et al., Moving from specifications to contracts in componentbased design, Lecture Notes in Computer Science, vol.7212, pp.43-58, 2012.

S. Sebastian, U. Bauer, L. Fahrenberg, K. G. Juhl, A. Larsen et al., Quantitative refinement for weighted modal transition systems, MFCS, pp.60-71, 2011.

S. Sebastian, U. Bauer, L. Fahrenberg, K. G. Juhl, A. Larsen et al., Weighted modal transition systems, Formal Methods in System Design, vol.42, issue.2, pp.193-220, 2013.

S. Sebastian, U. Bauer, A. Fahrenberg, C. Legay, and . Thrane, General quantitative specification theories with modalities, Lecture Notes in Computer Science, vol.7353, pp.18-30, 2012.

S. Sebastian, L. Bauer, K. G. Juhl, A. Larsen, J. Legay et al., Extending modal transition systems with structured labels, Mathematical Structures in Computer Science, vol.22, issue.4, pp.581-617, 2012.

S. Sebastian, L. Bauer, K. G. Juhl, J. Larsen, A. Srba et al., A logic for accumulated-weight reasoning on multiweighted modal automata, pp.77-84, 2012.

N. Bene?, J. Ivana?ernáivana?ivana?erná, and . K?etínsk´k?etínsk´y, Modal Transition Systems: Composition and LTL Model Checking, Lecture Notes in Computer Science, vol.6996, pp.228-242, 2011.
DOI : 10.1007/978-3-642-24372-1_17

N. Bene?, J. K?etínsk´k?etínsk´y, K. G. Larsen, M. H. Møller, and J. Srba, Dual-Priced Modal Transition Systems with Time Durations, Lecture Notes in Computer Science, vol.7180, pp.122-137, 2012.
DOI : 10.1007/978-3-642-28717-6_12

N. Bene?, J. K?etínsk´k?etínsk´y, K. G. Larsen, and J. Srba, On determinism in modal transition systems, Theoretical Computer Science, vol.410, issue.41, pp.4026-4043, 2009.
DOI : 10.1016/j.tcs.2009.06.009

N. Bertrand, A. Legay, S. Pinchinat, and J. Raclet, A Compositional Approach on Modal Specifications for Timed Systems, Lecture Notes in Computer Science, vol.5885, pp.679-697, 2009.
DOI : 10.1007/978-3-642-10373-5_35
URL : https://hal.archives-ouvertes.fr/inria-00418855

N. Bertrand, A. Legay, S. Pinchinat, and J. Raclet, Modal event-clock specifications for timed component-based design, Science of Computer Programming, vol.77, issue.12, pp.1212-1234, 2012.
DOI : 10.1016/j.scico.2011.01.007
URL : https://hal.archives-ouvertes.fr/hal-00752449

N. Bertrand, S. Pinchinat, and J. Raclet, Refinement and Consistency of Timed Modal Specifications, LATA, pp.152-163, 2009.
DOI : 10.1007/3-540-56922-7_21
URL : https://hal.archives-ouvertes.fr/inria-00424283

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

P. Bouyer, K. G. Larsen, N. Markey, O. Sankur, and C. R. Thrane, Timed Automata Can Always Be Made Implementable, Lecture Notes in Computer Science, 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

T. A. Pavol?ern´ypavol?pavol?ern´pavol?ern´y, A. Henzinger, and . Radhakrishna, Simulation distances, Lecture Notes in Computer Science, vol.6269, pp.253-268, 2010.

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

A. David, K. G. Larsen, A. Legay, U. Nyman, and A. W?sowski, Timed I/O automata, Proceedings of the 13th ACM international conference on Hybrid systems: computation and control, HSCC '10, pp.91-100, 2010.
DOI : 10.1145/1755952.1755967
URL : http://vbn.aau.dk/ws/files/58768871/HSCC2010cameraready.pdf

M. Luca-de-alfaro, M. Faella, and . 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

T. A. Luca-de-alfaro, R. Henzinger, and . Majumdar, Discounting the Future in Systems Theory, Lecture Notes in Computer Science, vol.2719, pp.1022-1037, 2003.
DOI : 10.1007/3-540-45061-0_79

J. Desharnais, F. Laviolette, and M. Tracol, Approximate analysis of probabilistic processes, QEST, pp.264-273, 2008.

L. Doyen, T. A. Henzinger, A. Legay, and D. Ni?kovi?, Robustness of Sequential Circuits, 2010 10th International Conference on Application of Concurrency to System Design, pp.77-84, 2010.
DOI : 10.1109/ACSD.2010.26

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, L. Juhl, K. G. Larsen, and J. Srba, Energy Games in Multiweighted Automata, Lecture Notes in Computer Science, vol.158, issue.1&2, pp.95-115, 2011.
DOI : 10.1016/0304-3975(95)00188-3
URL : https://hal.archives-ouvertes.fr/hal-01088043

U. Fahrenberg and A. Legay, A Robust Specification Theory for Modal Event-Clock Automata, of Electronic Proceedings in Theoretical Computer Science, pp.5-16, 2012.
DOI : 10.4204/EPTCS.87.2
URL : https://hal.archives-ouvertes.fr/hal-01087988

U. Fahrenberg, A. Legay, and C. Thrane, The quantitative linear-time?branchingtime spectrum, FSTTCS, volume 13 of Leibniz International Proceedings in Informatics Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, pp.103-114, 2011.

U. Fahrenberg, A. Legay, and A. W?sowski, Vision Paper: Make a Difference! (Semantically), MoDELS, pp.490-500, 2011.
DOI : 10.1007/978-3-540-88643-3_15
URL : https://hal.archives-ouvertes.fr/hal-01088049

U. Fahrenberg, C. Thrane, and K. G. Larsen, Distances for Weighted Transition Systems: Games and Properties, of Electronic Proceedings in Theoretical Computer Science, pp.134-147, 2011.
DOI : 10.4204/EPTCS.57.10
URL : https://hal.archives-ouvertes.fr/hal-01088053

P. Godefroid, M. Huth, and R. Jagadeesan, Abstraction-Based Model Checking Using Modal Transition Systems, Lecture Notes in Computer Science, vol.2154, pp.426-440, 2001.
DOI : 10.1007/3-540-44685-0_29
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.29.1604

A. Gruler, M. Leucker, and K. D. Scheidemann, Modeling and Model Checking Software Product Lines, Lecture Notes in Computer Science, vol.5051, pp.113-131, 2008.
DOI : 10.1007/978-3-540-68863-1_8
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.149.5754

O. Grumberg, M. Lange, M. Leucker, and S. Shoham, Don???t Know in the ??-Calculus, Lecture Notes in Computer Science, vol.3385, pp.233-249, 2005.
DOI : 10.1007/978-3-540-30579-8_16

V. Gupta, T. A. Henzinger, and R. Jagadeesan, Robust timed automata, Lecture Notes in Computer Science, vol.1201, pp.331-345, 1997.
DOI : 10.1007/BFb0014736

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

L. Juhl, K. G. Larsen, and J. Srba, Modal transition systems with weight intervals, The Journal of Logic and Algebraic Programming, vol.81, issue.4, pp.408-421, 2012.
DOI : 10.1016/j.jlap.2012.03.008

G. Kim and . Larsen, Modal specifications Automatic Verification Methods for Finite State Systems, Lecture Notes in Computer Science, vol.407, pp.232-246, 1989.

K. G. Larsen, U. Fahrenberg, and C. Thrane, Metrics for weighted transition systems: Axiomatization and complexity, Theoretical Computer Science, vol.412, issue.28, pp.3358-3369, 2011.
DOI : 10.1016/j.tcs.2011.04.003
URL : https://hal.archives-ouvertes.fr/hal-01088055

U. Nyman, Modal Transition Systems as the Basis for Interface Theories and Product Lines, 2008.

M. R. David and . Park, Concurrency and automata on infinite sequences, Theoretical Computer Science, pp.167-183

J. Illum-rasmussen, K. G. Larsen, and K. Subramani, On using priced timed automata to achieve optimal scheduling, Formal Methods in System Design, vol.29, issue.1, pp.97-114, 2006.
DOI : 10.1007/s10703-006-0014-1

M. Swaminathan and M. Fränzle, A Symbolic Decision Procedure for Robust Safety of Timed Systems, 14th International Symposium on Temporal Representation and Reasoning (TIME'07), p.192, 2007.
DOI : 10.1109/TIME.2007.39

M. Swaminathan, M. Fränzle, and J. Katoen, The Surprising Robustness of (Closed) Timed Automata against Clock-Drift, IFIP TCS, pp.537-553, 2008.
DOI : 10.1007/978-0-387-09680-3_36

A. Tarski, A lattice-theoretical fixpoint theorem and its applications, Pacific Journal of Mathematics, vol.5, issue.2, pp.285-309, 1955.
DOI : 10.2140/pjm.1955.5.285

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

. Franck-van-breugel, A Theory of Metric Labelled Transition Systems, Annals of the New York Academy of Sciences, vol.5, issue.1, pp.69-87, 1996.
DOI : 10.2307/1990864

. Franck-van-breugel, A Behavioural Pseudometric for Metric Labelled Transition Systems, Lecture Notes in Computer Science, vol.3653, pp.141-155, 2005.
DOI : 10.1007/11539452_14

G. Winskel and M. Nielsen, Models for concurrency, Handbook of Logic in Computer Science, pp.1-148, 1995.

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