Probabilistic Opacity for Markov Decision Processes

Béatrice Bérard, Krishnendu Chatterjee, Nathalie Sznajder

Opacity is a generic security property, that has been defined on (non probabilistic) transition systems and later on Markov chains with labels. For a secret predicate, given as a s…