Probabilistic Opacity in Refinement-Based Modeling

Béatrice Bérard, Olga Kouchnarenko, John Mullins +1

Given a probabilistic transition system (PTS) $\mathcal{A}$ partially observed by an attacker, and an $\omega$-regular predicate $\phi$over the traces of $\mathcal{A}$, measuring the disclosure of t…