# Non-Deterministic Planning for Hyperproperty Verification

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

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Builds on 7 of its 28 references that are in the map.
- First posted on arXiv 22 May 2024.

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

- [Temporal Logics for Hyperproperties](https://mlsanity.com/paper/1401.4492/) (2014)
- [Compact Policies for Fully-Observable Non-Deterministic Planning as SAT](https://mlsanity.com/paper/1806.09455/) (2018)
- [AutoHyper: Explicit-State Model Checking for HyperLTL](https://mlsanity.com/paper/2301.11229/) (2023)
- [Flexible FOND Planning with Explicit Fairness Assumptions](https://mlsanity.com/paper/2103.08391/) (2021)
- [Bounded Model Checking for Hyperproperties](https://mlsanity.com/paper/2009.08907/) (2020)
- [Software Verification of Hyperproperties Beyond k-Safety](https://mlsanity.com/paper/2206.03381/) (2022)
- [Efficient Loop Conditions for Bounded Model Checking Hyperproperties](https://mlsanity.com/paper/2301.06209/) (2023)

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

- [HypRL: Reinforcement Learning of Control Policies for Hyperproperties](https://mlsanity.com/paper/2504.04675/) (2025)
- [Decentralized Planning Using Probabilistic Hyperproperties](https://mlsanity.com/paper/2502.13621/) (2025)
- [On Conformant Planning and Model-Checking of exists^*forall^* Hyperproperties](https://mlsanity.com/paper/2512.23324/) (2025)
- [HyPOLE: Hyperproperty-Guided Multi-Agent Reinforcement Learning under Partial Observation](https://mlsanity.com/paper/2606.30966/) (2026)

## Abstract (arXiv)

Non-deterministic planning aims to find a policy that achieves a given objective in an environment where actions have uncertain effects, and the agent - potentially - only observes parts of the current state. Hyperproperties are properties that relate multiple paths of a system and can, e.g., capture security and information-flow policies. Popular logics for expressing temporal hyperproperties - such as HyperLTL - extend LTL by offering selective quantification over executions of a system. In this paper, we show that planning offers a powerful intermediate language for the automated verification of hyperproperties. Concretely, we present an algorithm that, given a HyperLTL verification problem, constructs a non-deterministic multi-agent planning instance (in the form of a QDec-POMDP) that, when admitting a plan, implies the satisfaction of the verification problem. We show that for large fragments of HyperLTL, the resulting planning instance corresponds to a classical, FOND, or POND planning problem. We implement our encoding in a prototype verification tool and report on encouraging experimental results.