# Probabilistic Hyperproperties of Markov Decision Processes

arXiv: https://arxiv.org/abs/2005.03362 · HTML: https://mlsanity.com/paper/2005.03362/

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 7 May 2020.

## Built on by (most cited first, 6 of 6)

- [Monitoring Algorithmic Fairness](https://mlsanity.com/paper/2305.15979/) (2023)
- [Causal Temporal Reasoning for Markov Decision Processes](https://mlsanity.com/paper/2212.08712/) (2022)
- [Counterfactuals Modulo Temporal Logics](https://mlsanity.com/paper/2306.08916/) (2023)
- [Deductive Controller Synthesis for Probabilistic Hyperproperties](https://mlsanity.com/paper/2307.04503/) (2023)
- [Decentralized Planning Using Probabilistic Hyperproperties](https://mlsanity.com/paper/2502.13621/) (2025)
- [Sample-Efficient Learning of Probabilistic Causes for Reachability in Markov Decision Processes with Probabilistic Guarantees](https://mlsanity.com/paper/2606.29681/) (2026)

## Abstract (arXiv)

Hyperproperties are properties that describe the correctness of a system as a relation between multiple executions. Hyperproperties generalize trace properties and include information-flow security requirements, like noninterference, as well as requirements like symmetry, partial observation, robustness, and fault tolerance. We initiate the study of the specification and verification of hyperproperties of Markov decision processes (MDPs). We introduce the temporal logic PHL (Probabilistic Hyper Logic), which extends classic probabilistic logics with quantification over schedulers and traces. PHL can express a wide range of hyperproperties for probabilistic systems, including both classical applications, such as probabilistic noninterference, and novel applications in areas such as robotics and planning. While the model checking problem for PHL is in general undecidable, we provide methods both for proving and for refuting formulas from a fragment of the logic. The fragment includes many probabilistic hyperproperties of interest.