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, Proc. of the 33rd Intl. Colloquium on Automata, Languages and Programming (ICALP'06, pp.107-118, 2006.
DOI : 10.1007/11787006_10

L. Mazaré, Decidability of Opacity with Non-Atomic Keys, Proc. 2nd Workshop on Formal Aspects in Security and Trust 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

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, Foundations of Software Science and Computation Structure (FoSSaCS) 2008, pp.302-317, 2008.

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

P. Billingsley, Probability and Measure, 1995.

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

C. Courcoubetis and M. Yannakakis, The complexity of probabilistic verification, Journal of the ACM, vol.42, issue.4, pp.857-907, 1995.
DOI : 10.1145/210332.210339

B. Bérard, J. Mullins, and M. Sassolas, Quantifying opacity, Proceedings of the 7th International Conference on Quantitative Evaluation of Systems (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, Proceedings of the 16th International Conference on Concurrency Theory (CONCUR'05, pp.171-185, 2005.
DOI : 10.1007/11539452_16
URL : https://hal.archives-ouvertes.fr/inria-00201101

N. Piterman, From nondeterministic Büchi and Streett automata to deterministic parity automata, Logical Methods in Computer Science, vol.3, issue.3, 2007.