Tractable Hyperproperties for MDPs
This work addresses the verification of security and privacy policies in stochastic systems, offering a practical solution for an underexplored problem, though it is incremental as it focuses on specific fragments rather than the general case.
The paper tackles the problem of verifying probabilistic hyperproperties in Markov decision processes (MDPs), which was previously undecidable, by focusing on tractable fragments that relate probabilities of events across executions, and it provides efficient algorithms with an implementation that outperforms existing solvers by orders of magnitude on relevant benchmarks.
Probabilistic hyperproperties describe probabilistic relations between multiple sets of executions in a stochastic system. Prominent examples include information-theoretic characterizations of security and privacy policies. However, model checking for existing probabilistic hyperlogics, such as HyperPCTL and PHL, is undecidable in Markov decision processes (MDPs). In this paper, we study an underexplored problem: the verification of fragments of probabilistic hyperproperties that relate the probabilities of different events to each other, possibly across independent executions of an MDP. Representative verification questions include: Can two different target states be reached from the same initial state with the same probability? (different events), Can a given target state be reached from two different initial states with the same probability? (same event, independent executions), and natural combinations of these forms. Besides reachability, our relational probabilistic properties cover safety, Büchi, and coBüchi objectives. They can also be combined conjunctively, thereby generalizing standard multi-objective MDP properties. We provide efficient algorithms for relevant classes of relational properties, while proving computational hardness and completeness results for others. An implementation of our approach outperforms solvers for more general probabilistic hyperlogics by orders of magnitude on the subset of their benchmarks that lies within our fragment.