# Decentralized Planning Using Probabilistic Hyperproperties

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 12 of its 49 references that are in the map.
- First posted on arXiv 19 Feb 2025.

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

- [The Complexity of Decentralized Control of Markov Decision Processes](https://mlsanity.com/paper/1301.3836/) (2013)
- [From Spot 2.0 to Spot 2.10: What's New?](https://mlsanity.com/paper/2206.11366/) (2022)
- [Temporal Logics for Hyperproperties](https://mlsanity.com/paper/1401.4492/) (2014)
- [Strategy Logic with Imperfect Information](https://mlsanity.com/paper/1805.12592/) (2018)
- [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)
- [Solving infinite-horizon Dec-POMDPs using Finite State Controllers within JESP](https://mlsanity.com/paper/2109.08755/) (2021)
- [Non-Deterministic Planning for Hyperproperty Verification](https://mlsanity.com/paper/2405.13488/) (2024)
- [Opacity of nondeterministic transition systems: A (bi)simulation relation approach](https://mlsanity.com/paper/1802.03321/) (2018)
- [Strategic Abilities of Forgetful Agents in Stochastic Environments](https://mlsanity.com/paper/2310.17240/) (2023)
- [Deductive Controller Synthesis for Probabilistic Hyperproperties](https://mlsanity.com/paper/2307.04503/) (2023)

## Abstract (arXiv)

Multi-agent planning under stochastic dynamics is usually formalised using decentralized (partially observable) Markov decision processes ( MDPs) and reachability or expected reward specifications. In this paper, we propose a different approach: we use an MDP describing how a single agent operates in an environment and probabilistic hyperproperties to capture desired temporal objectives for a set of decentralized agents operating in the environment. We extend existing approaches for model checking probabilistic hyperproperties to handle temporal formulae relating paths of different agents, thus requiring the self-composition between multiple MDPs. Using several case studies, we demonstrate that our approach provides a flexible and expressive framework to broaden the specification capabilities with respect to existing planning techniques. Additionally, we establish a close connection between a subclass of probabilistic hyperproperties and planning for a particular type of Dec-MDPs, for both of which we show undecidability. This lays the ground for the use of existing decentralized planning tools in the field of probabilistic hyperproperty verification.