# Deductive Controller Synthesis for Probabilistic Hyperproperties

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 15 of its 37 references that are in the map.
- First posted on arXiv 10 Jul 2023.

## Builds on (most cited first, 15 of 15)

- [The Probabilistic Model Checker Storm](https://mlsanity.com/paper/2002.07080/) (2020)
- [Temporal Logics for Hyperproperties](https://mlsanity.com/paper/1401.4492/) (2014)
- [Permissive Controller Synthesis for Probabilistic Systems](https://mlsanity.com/paper/1504.04662/) (2015)
- [Inductive Synthesis of Finite-State Controllers for POMDPs](https://mlsanity.com/paper/2203.10803/) (2022)
- [Probabilistic Hyperproperties of Markov Decision Processes](https://mlsanity.com/paper/2005.03362/) (2020)
- [Hyperproperties for Robotics: Planning via HyperLTL](https://mlsanity.com/paper/1911.11870/) (2019)
- [Shepherding Hordes of Markov Chains](https://mlsanity.com/paper/1902.05727/) (2019)
- [HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties](https://mlsanity.com/paper/1804.01853/) (2018)
- [On probability-raising causality in Markov decision processes](https://mlsanity.com/paper/2201.08768/) (2022)
- [Software Verification of Hyperproperties Beyond k-Safety](https://mlsanity.com/paper/2206.03381/) (2022)
- [Verification and Control of Partially Observable Probabilistic Real-Time Systems](https://mlsanity.com/paper/1506.06419/) (2015)
- [Synthesizing Reactive Systems from Hyperproperties](https://mlsanity.com/paper/1905.13511/) (2019)
- [Probabilistic Hyperproperties with Nondeterminism](https://mlsanity.com/paper/2005.06115/) (2020)
- [Controller Synthesis for Hyperproperties](https://mlsanity.com/paper/2101.08880/) (2021)
- [Inductive Synthesis for Probabilistic Programs Reaches New Horizons](https://mlsanity.com/paper/2101.12683/) (2021)

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

- [Decentralized Planning Using Probabilistic Hyperproperties](https://mlsanity.com/paper/2502.13621/) (2025)

## Abstract (arXiv)

Probabilistic hyperproperties specify quantitative relations between the probabilities of reaching different target sets of states from different initial sets of states. This class of behavioral properties is suitable for capturing important security, privacy, and system-level requirements. We propose a new approach to solve the controller synthesis problem for Markov decision processes (MDPs) and probabilistic hyperproperties. Our specification language builds on top of the logic HyperPCTL and enhances it with structural constraints over the synthesized controllers. Our approach starts from a family of controllers represented symbolically and defined over the same copy of an MDP. We then introduce an abstraction refinement strategy that can relate multiple computation trees and that we employ to prune the search space deductively. The experimental evaluation demonstrates that the proposed approach considerably outperforms HyperProb, a state-of-the-art SMT-based model checking tool for HyperPCTL. Moreover, our approach is the first one that is able to effectively combine probabilistic hyperproperties with additional intra-controller constraints (e.g. partial observability) as well as inter-controller constraints (e.g. agreements on a common action).