Tractable Hyperproperties for MDPs

TL;DR

This paper introduces efficient algorithms for verifying specific fragments of probabilistic hyperproperties in Markov decision processes, addressing previously undecidable problems and outperforming existing solvers.

Contribution

It identifies tractable subclasses of probabilistic hyperproperties in MDPs and provides algorithms with proven complexity results and practical implementation.

Findings

Efficient algorithms for certain relational hyperproperties in MDPs.

Proven computational hardness for other classes of hyperproperties.

Implementation outperforms existing solvers on targeted benchmarks.

Abstract

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\"uchi, and coB\"uchi 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.