# HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 5 Apr 2018.

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

- [Counterfactuals Modulo Temporal Logics](https://mlsanity.com/paper/2306.08916/) (2023)
- [Deductive Controller Synthesis for Probabilistic Hyperproperties](https://mlsanity.com/paper/2307.04503/) (2023)
- [Property-driven Causal Abstractions for Markov Decision Processes](https://mlsanity.com/paper/2607.26787/) (2026)

## Abstract (arXiv)

In this paper, we propose a new logic for expressing and reasoning about probabilistic hyperproperties. Hyperproperties characterize the relation between different independent executions of a system. Probabilistic hyperproperties express quantitative dependencies between such executions. The standard temporal logics for probabilistic systems, i.e., PCTL and PCTL* can refer only to a single path at a time and, hence, cannot express many probabilistic hyperproperties of interest. The logic proposed in this paper, HyperPCTL, adds explicit and simultaneous quantification over multiple traces to PCTL. Such quantification allows expressing probabilistic hyperproperties. A model checking algorithm for the proposed logic is also given for discrete-time Markov chains.