L. Aceto, I. Fábregas, D. De-frutos-escrig, A. Ingólfsdóttir, and M. Palomino, On the specification of modal systems: A comparison of three frameworks, Science of Computer Programming, vol.78, issue.12, pp.2468-2487, 2013.
DOI : 10.1016/j.scico.2013.02.004

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

S. Sebastian, A. Bauer, R. David, K. G. Hennicker, A. Larsen et al., Moving from specifications to contracts in component-based design, Lect. Notes Comput. Sci, vol.7212, pp.43-58, 2012.

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

S. Sebastian, L. Bauer, K. G. Juhl, A. Larsen, J. Legay et al., Extending modal transition systems with structured labels, Math. Struct. Comput. Sci, vol.22, issue.4, pp.581-617, 2012.

S. Ben-david, M. Chechik, and S. Uchitel, Merging Partial Behaviour Models with Different Vocabularies, pp.91-105
DOI : 10.1007/978-3-642-40184-8_8

N. Bene?, B. Delahaye, U. F. K?etínský, and A. Legay, Hennessy-Milner logic with greatest fixed points, pp.76-90

N. Bene?, J. K?etínský, 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. Bene?, I. ?erná, and J. K?etínský, Modal Transition Systems: Composition and LTL Model Checking, ATVA, pp.228-242, 2011.
DOI : 10.1007/978-3-642-24372-1_17

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

G. Boudol and K. G. Larsen, Graphical versus logical specifications, Theoretical Computer Science, vol.106, issue.1, pp.3-20, 1992.
DOI : 10.1016/0304-3975(92)90276-L

URL : https://hal.archives-ouvertes.fr/inria-00075455

B. Caillaud, B. Delahaye, K. G. Larsen, A. Legay, M. L. Pedersen et al., Constraint Markov Chains, Theoretical Computer Science, vol.412, issue.34, pp.4373-4404, 2011.
DOI : 10.1016/j.tcs.2011.05.010

URL : https://hal.archives-ouvertes.fr/hal-00654003

L. Caires and L. Cardelli, A spatial logic for concurrency (part I), Information and Computation, vol.186, issue.2, pp.194-235, 2003.
DOI : 10.1016/S0890-5401(03)00137-8

L. Cardelli, K. G. Larsen, and R. Mardare, Modular Markovian Logic, Lect. Notes Comput. Sci, vol.6756, issue.2, pp.380-391, 2011.
DOI : 10.1142/p595

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.190.5515

R. D. Pedro, H. C. Argenio, and . Melgratti, CON- CUR 2013 -Concurrency Theory -24th Int, Conf. Lect. Notes Comput. Sci, vol.8052, 2013.

A. David, K. G. Larsen, A. Legay, U. Nyman, L. Traonouez et al., Realtime specifications, Int. J
URL : https://hal.archives-ouvertes.fr/hal-01087799

A. Luca-de, Quantitative verification and control via the mu-calculus, Lect. Notes Comput. Sci, vol.2761, pp.102-126, 2003.

M. Luca-de-alfaro, T. A. Faella, R. Henzinger, M. Majumdar, and . 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

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

L. De, A. , and T. A. Henzinger, Interface automata, ESEC / SIGSOFT FSE, pp.109-120, 2001.

T. A. Luca-de-alfaro, M. Henzinger, and . Stoelinga, Timed Interfaces, Lect. Notes Comput. Sci, vol.2491, pp.108-122, 2002.
DOI : 10.1007/3-540-45828-X_9

U. Benoît-delahaye, K. G. Fahrenberg, A. Larsen, and . Legay, Refinement and difference for probabilistic automata, Logical Methods in Computer Science, vol.10, issue.3, p.2014

K. G. Benoît-delahaye, A. Larsen, M. L. Legay, A. Pedersen, and . W?sowski, Consistency and refinement for Interval Markov Chains, The Journal of Logic and Algebraic Programming, vol.81, issue.3, pp.209-226, 2012.
DOI : 10.1016/j.jlap.2011.10.003

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

U. Fahrenberg, M. Acher, A. Legay, and A. W?sowski, Sound Merging and Differencing for Class Diagrams, Lect. Notes Comput. Sci, vol.8411, pp.63-78, 2014.
DOI : 10.1007/978-3-642-54804-8_5

URL : https://hal.archives-ouvertes.fr/hal-01087323

U. Fahrenberg, J. K?etínský, A. Legay, and L. Traonouez, Compositionality for quantitative specifications, FACS, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01088154

U. Fahrenberg and A. Legay, A Robust Specification Theory for Modal Event-Clock Automata, Electronic Proceedings in Theoretical Computer Science, vol.87, issue.6, pp.5-16
DOI : 10.4204/EPTCS.87.2

URL : https://hal.archives-ouvertes.fr/hal-01087988

U. Fahrenberg and A. Legay, Generalized Quantitative Analysis of Metric Transition Systems, Lect. Notes Comput. Sci, vol.8301, pp.192-208, 2013.
DOI : 10.1007/978-3-319-03542-0_14

URL : https://hal.archives-ouvertes.fr/hal-01087911

U. Fahrenberg and A. Legay, General quantitative specification theories with modal transition systems, Acta Informatica, vol.806, issue.1, pp.261-295, 2014.
DOI : 10.1007/s00236-014-0196-8

URL : https://hal.archives-ouvertes.fr/hal-01087314

U. Fahrenberg and A. Legay, The quantitative linear-time???branching-time spectrum, Theoretical Computer Science, vol.538, pp.54-69, 2014.
DOI : 10.1016/j.tcs.2013.07.030

URL : https://hal.archives-ouvertes.fr/hal-01087368

U. Fahrenberg, A. Legay, and L. Traonouez, Structural Refinement for the Modal nu-Calculus, Lect. Notes Comput. Sci, vol.8687, pp.169-187, 2014.
DOI : 10.1007/978-3-319-10882-7_11

URL : https://hal.archives-ouvertes.fr/hal-01087295

J. Girard, Linear logic, Theoretical Computer Science, vol.50, issue.1, pp.1-102, 1987.
DOI : 10.1016/0304-3975(87)90045-4

URL : https://hal.archives-ouvertes.fr/inria-00075966

M. Hennessy, Acceptance trees, Journal of the ACM, vol.32, issue.4, pp.896-928, 1985.
DOI : 10.1145/4221.4249

T. A. Henzinger, R. Majumdar, and V. S. Prabhu, Quantifying Similarities Between Timed Systems, Lect. Notes Comput. Sci, vol.3829, pp.226-241, 2005.
DOI : 10.1007/11603009_18

A. Thomas, J. Henzinger, and . Sifakis, The embedded systems design challenge, Lect. Notes Comput. Sci, vol.4085, pp.1-15, 2006.

M. Huth and M. Z. Kwiatkowska, Quantitative analysis and model checking, Proceedings of Twelfth Annual IEEE Symposium on Logic in Computer Science, pp.111-122, 1997.
DOI : 10.1109/LICS.1997.614940

B. Jacobs and E. Poll, A Logic for the Java Modeling Language JML, Lect. Notes Comput. Sci, vol.2029, pp.284-299, 2001.
DOI : 10.1007/3-540-45314-8_21

B. Jonsson and K. G. Larsen, Specification and refinement of probabilistic processes, [1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science, pp.266-277, 1991.
DOI : 10.1109/LICS.1991.151651

B. Klin and V. Sassone, Structural operational semantics for stochastic and weighted transition systems, Information and Computation, vol.227, pp.58-83, 2013.
DOI : 10.1016/j.ic.2013.04.001

J. K?etínský and S. Sickert, MoTraS: A Tool for Modal Transition Systems and Their Extensions, Lect. Notes Comput. Sci, vol.8172, pp.487-491, 2013.
DOI : 10.1007/978-3-319-02444-8_41

G. Kim and . Larsen, Proof systems for satisfiability in Hennessy-Milner logic with recursion, Theor. Comput. Sci, vol.72, issue.2&3, pp.265-288, 1990.

K. G. Larsen, A. Legay, L. Traonouez, and A. W?sowski, Robust Specification of Real Time Components, Lect. Notes Comput. Sci, vol.17, issue.3, pp.129-144, 2011.
DOI : 10.1007/s00165-005-0067-8

URL : https://hal.archives-ouvertes.fr/hal-01088002

K. G. Larsen, A. Legay, L. Traonouez, and A. W?sowski, Robust synthesis for real-time systems, Theoretical Computer Science, vol.515, pp.96-122, 2014.
DOI : 10.1016/j.tcs.2013.08.015

URL : https://hal.archives-ouvertes.fr/hal-01087778

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

G. Kim, B. Larsen, and . Thomsen, A modal process logic, LICS, pp.203-210, 1988.

G. Kim, L. Larsen, and . Xinxin, Equation solving using modal transition systems, LICS, pp.108-117, 1990.

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

B. Liskov and J. M. Wing, A behavioral notion of subtyping, ACM Transactions on Programming Languages and Systems, vol.16, issue.6, pp.1811-1841, 1994.
DOI : 10.1145/197320.197383

M. Mio, Probabilistic Modal ??-Calculus with Independent Product, Lect. Notes Comput. Sci, vol.6604, pp.290-304, 2011.
DOI : 10.1007/978-3-642-19805-2_20

URL : https://hal.archives-ouvertes.fr/hal-00763451

C. Morgan and A. Mciver, A probabilistic temporal calculus based on expectations, Formal Methods Pathific, 1997.

J. Raclet, Residual for Component Specifications, Electronic Notes in Theoretical Computer Science, vol.215, 2007.
DOI : 10.1016/j.entcs.2008.06.023

URL : https://hal.archives-ouvertes.fr/inria-00141898

D. Romero-hernández and D. De-frutos-escrig, Defining Distances for All Process Semantics
DOI : 10.1007/978-3-642-30793-5_11

D. Romero-hernández and D. De-frutos-escrig, Distances between Processes: A Pure Algebraic Approach, Lect. Notes Comput. Sci, vol.7841, pp.265-282, 2012.
DOI : 10.1007/978-3-642-37635-1_16

J. Sifakis, A vision for computer science -the system perspective. Central Europ, J. Comput. Sci, vol.1, issue.1, pp.108-116, 2011.

L. Traonouez, A Parametric Counterexample Refinement Approach for Robust Timed Specifications, Electronic Proceedings in Theoretical Computer Science, vol.87, issue.6, pp.17-33
DOI : 10.4204/EPTCS.87.3

URL : https://hal.archives-ouvertes.fr/hal-01088011

S. Uchitel and M. Chechik, Merging partial behavioural models, SIGSOFT FSE, pp.43-52, 2004.
DOI : 10.1145/1041685.1029904

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.100.4666

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

P. ?erný, T. A. Henzinger, and A. Radhakrishna, Simulation distances, Theoretical Computer Science, vol.413, issue.1, pp.21-35, 2012.
DOI : 10.1016/j.tcs.2011.08.002