Probabilistic Opacity for Markov Decision Processes

Opacity is a generic security property, that has been defined on (non probabilistic) transition systems and later on Markov chains with labels. We extend the definition of opacity to the richer framework of Markov decision processes, where non deterministic choice is combined with probabilistic transitions and we study related decidability problems with partial or complete observation hypotheses for the schedulers. We prove that all questions are decidable with complete observation. With partial observation, we prove that all quantitative questions are undecidable but the question whether a system is almost surely non opaque remains decidable.