M. R. Clarkson and F. B. Schneider, Hyperproperties, Journal of Computer Security, vol.18, issue.6, pp.1157-1210, 2010.
DOI : 10.3233/JCS-2009-0393

R. Alur, P. Cern´ycern´y, and S. Zdancewic, Preserving Secrecy Under Refinement
DOI : 10.1007/11787006_10

L. Mazaré, Decidability of Opacity with Non-Atomic Keys, Proc. FAST'04. Volume 173 of Intl. Federation for Information Processing, pp.71-84, 2005.
DOI : 10.1007/0-387-24098-5_6

J. W. Bryans, M. Koutny, L. Mazaré, and P. Y. Ryan, Opacity generalised to transition systems, International Journal of Information Security, vol.79, issue.3???4, pp.421-435, 2008.
DOI : 10.1007/s10207-008-0058-x

A. Saboori and C. N. Hadjicostis, Current-State Opacity Formulations in Probabilistic Finite Automata, IEEE Transactions on Automatic Control, vol.59, issue.1, pp.120-133, 2014.
DOI : 10.1109/TAC.2013.2279914

B. Bérard, J. Mullins, and M. Sassolas, Quantifying opacity, Mathematical Structures in Computer Science, vol.12, issue.02, pp.361-403, 2015.
DOI : 10.1016/j.ic.2007.07.003

B. Bérard, K. Chatterjee, and N. Sznajder, Probabilistic opacity for Markov decision processes, Information Processing Letters, vol.115, issue.1, pp.52-59, 2015.
DOI : 10.1016/j.ipl.2014.09.001

C. Baier, J. P. Katoen, H. Hermanns, and V. Wolf, Comparative branching-time semantics for Markov chains, Information and Computation, vol.200, issue.2, pp.149-214, 2005.
DOI : 10.1016/j.ic.2005.03.001

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

R. Segala, Modeling and Verification of Randomized Distributed Real-Time Systems, 1995.

K. Chatterjee, T. Henzinger, and K. Sen, Model-checking omega-regular properties of interval Markov chains, Proc. FoSSaCS'08, pp.302-317, 2008.

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

M. Benedikt, R. Lenhardt, and J. Worrell, LTL Model Checking of Interval Markov Chains, Proc. TACAS'13, pp.32-46, 2013.
DOI : 10.1007/978-3-642-36742-7_3

B. Delahaye, Consistency for parametric interval Markov chains, Proc. SynCoP'15, pp.17-32, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01140752

B. Bérard, O. Kouchnarenko, J. Mullins, and M. Sassolas, Preserving opacity on Interval Markov Chains under simulation, 2016 13th International Workshop on Discrete Event Systems (WODES), pp.319-324, 2016.
DOI : 10.1109/WODES.2016.7497866

P. Billingsley, Probability and Measure, 1995.

B. Bérard, J. Mullins, and M. Sassolas, Quantifying opacity, Proc. QEST'10, pp.263-272, 2010.

D. Chaum, The dining cryptographers problem: Unconditional sender and recipient untraceability, Journal of Cryptology, vol.1, issue.1, pp.65-75, 1988.
DOI : 10.1007/BF00206326

M. Bhargava and C. Palamidessi, Probabilistic Anonymity, Proc. CONCUR'05, pp.171-185, 2005.
DOI : 10.1007/11539452_16
URL : https://hal.archives-ouvertes.fr/inria-00201101

F. Biondi, A. Legay, B. F. Nielsen, and A. W¸asowskiw¸asowski, Maximizing entropy over Markov processes, Journal of Logical and Algebraic Methods in Programming, vol.83, pp.5-6, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01242613

C. Roos, T. Terlaky, and J. P. Vial, Theory and Algorithms for Linear Optimization. An Interior Point Approach, 1997.

K. Sen, M. Viswanathan, and G. Agha, Model-Checking Markov Chains in the Presence of Uncertainties, Proc. of 12th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, TACAS'06, pp.394-410, 2006.
DOI : 10.1016/0004-3702(95)00009-7

N. Piterman, From Nondeterministic Büchi and Streett Automata to Deterministic Parity Automata, Logical Methods in Computer Science, vol.3, issue.3, 2007.

C. Baier and J. P. Katoen, Principles of Model Checking (Representation and Mind Series), 2008.