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

H. Aljazzar and S. Leue, Directed Explicit State-Space Search in the Generation of Counterexamples for Stochastic Model Checking, IEEE Transactions on Software Engineering, vol.36, issue.1, 2010.
DOI : 10.1109/TSE.2009.57

R. Alur, T. Feder, and T. A. Henzinger, The benefits of relaxing punctuality, Journal of the ACM, vol.43, issue.1, pp.116-146, 1996.
DOI : 10.1145/227595.227602

M. E. Andrés, P. R. Argenio, and P. Van-rossum, Significant Diagnostic Counterexamples in Probabilistic Model Checking, HVC, pp.129-148, 2008.
DOI : 10.1007/978-3-540-24611-4_1

C. Baier and J. Katoen, Principles of Model Checking, 2008.

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

M. M. Bonsangue, F. Van-breugel, and J. J. Rutten, Generalized metric spaces: Completion, topology, and powerdomains via the Yoneda embedding, Theoretical Computer Science, vol.193, issue.1-2, pp.1-51, 1998.
DOI : 10.1016/S0304-3975(97)00042-X

R. Chadha and M. Viswanathan, A counterexample-guided abstraction-refinement framework for markov decision processes, ACM Transactions on Computational Logic, vol.12, issue.1, 2010.
DOI : 10.1145/1838552.1838553

J. M. Cobleigh, G. S. Avrunin, and L. A. Clarke, Breaking up is hard to do, ACM Transactions on Software Engineering and Methodology, vol.17, issue.2, 2008.
DOI : 10.1145/1348250.1348253

J. M. Cobleigh, D. Giannakopoulou, and C. S. Pasareanu, Learning Assumptions for Compositional Verification, TACAS, pp.331-346, 2003.
DOI : 10.1007/3-540-36577-X_24

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

L. De-alfaro, R. Majumdar, V. Raman, and M. Stoelinga, Game Relations and Metrics, 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), pp.99-108, 2007.
DOI : 10.1109/LICS.2007.22

B. Delahaye, J. Katoen, K. G. Larsen, A. Legay, M. L. Pedersen et al., Abstract probabilistic automata, VMCAI, pp.324-339, 2011.
URL : https://hal.archives-ouvertes.fr/hal-01084342

B. Delahaye, J. Katoen, K. G. Larsen, A. Legay, M. L. Pedersen et al., New Results on Abstract Probabilistic Automata, 2011 Eleventh International Conference on Application of Concurrency to System Design, pp.118-127, 2011.
DOI : 10.1109/ACSD.2011.10

B. Delahaye, K. G. Larsen, A. Legay, M. L. Pedersen, and A. Wasowski, APAC: A Tool for Reasoning about Abstract Probabilistic Automata, 2011 Eighth International Conference on Quantitative Evaluation of SysTems, pp.151-152, 2011.
DOI : 10.1109/QEST.2011.28

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

H. Fecher, M. Leucker, and V. Wolf, Don???t Know in Probabilistic Systems, In SPIN LNCS, vol.60, issue.1???4, pp.71-88, 2006.
DOI : 10.1007/3-540-58468-4_190

T. Han, J. Katoen, and B. Damman, Counterexample generation in probabilistic model checking, IEEE Trans. Software Eng, vol.35, issue.2, pp.241-257, 2009.

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

H. Hermanns, U. Herzog, and J. Katoen, Process algebra for performance evaluation, Theoretical Computer Science, vol.274, issue.1-2, pp.43-87, 2002.
DOI : 10.1016/S0304-3975(00)00305-4

A. Hinton, M. Z. Kwiatkowska, G. Norman, and D. Parker, PRISM: A Tool for Automatic Verification of Probabilistic Systems, TACAS, 2006.
DOI : 10.1007/11691372_29

N. Jansen, E. Ábrahám, J. Katelaan, R. Wimmer, J. Katoen et al., Hierarchical Counterexamples for Discrete-Time Markov Chains, ATVA, 2011.
DOI : 10.1007/978-3-642-24372-1_33

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

J. Katoen, D. Klink, M. Leucker, and V. Wolf, Three-Valued Abstraction for Continuous-Time Markov Chains, CAV, pp.311-324, 2007.
DOI : 10.1007/978-3-540-73368-3_37

A. Komuravelli, C. S. Pasareanu, and E. M. Clarke, Assume-Guarantee Abstraction Refinement for Probabilistic Systems, In CAV LNCS, vol.7358, pp.310-326, 2012.
DOI : 10.1007/978-3-642-31424-7_25

M. Z. Kwiatkowska, G. Norman, D. Parker, and H. Qu, Assume-Guarantee Verification for Probabilistic Systems, TACAS, 2010.
DOI : 10.1007/978-3-642-12002-2_3
URL : https://hal.archives-ouvertes.fr/inria-00458058

K. G. Larsen, Modal specifications, AVMS, pp.232-246, 1989.
DOI : 10.1007/3-540-52148-8_19

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

N. Lynch and M. R. Tuttle, An introduction to Input/Output automata, CWI, vol.2, issue.3, 1989.

N. A. Lynch, Distributed Algorithms, 1996.

Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems, 1992.
DOI : 10.1007/978-1-4612-0931-7

J. Raclet, Quotient de spécifications pour la réutilisation de composants, 2007.

M. Sassolas, M. Chechik, and S. Uchitel, Exploring inconsistencies between modal transition systems, Software & Systems Modeling, vol.35, issue.3, pp.117-142, 2011.
DOI : 10.1007/s10270-010-0148-x
URL : https://hal.archives-ouvertes.fr/hal-01161870

M. Schmalz, D. Varacca, and H. Völzer, Counterexamples in Probabilistic LTL Model Checking for Markov Chains, In CONCUR LNCS, vol.6, issue.5, 2009.
DOI : 10.1007/978-3-540-93900-9_29

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

F. Sher and J. Katoen, Compositional Abstraction Techniques for Probabilistic Automata, IFIP TCS, pp.325-341, 2012.
DOI : 10.1007/978-3-642-33475-7_23

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, M. W. Mislove, J. Ouaknine, and J. Worrell, An Intrinsic Characterization of Approximate Probabilistic Bisimilarity, FoSSaCS, pp.200-215, 2003.
DOI : 10.1007/3-540-36576-1_13

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

R. Wimmer, B. Braitling, and B. Becker, Counterexample Generation for Discrete-Time Markov Chains Using Bounded Model Checking, VMCAI, 2009.
DOI : 10.1007/978-3-540-93900-9_29

R. Wimmer, N. Jansen, E. Ábrahám, B. Becker, and J. Katoen, Minimal Critical Subsystems for Discrete-Time Markov Models, TACAS, 2012.
DOI : 10.1007/978-3-642-28756-5_21