# On Conformant Planning and Model-Checking of exists^*forall^* Hyperproperties

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 11 of its 37 references that are in the map.
- First posted on arXiv 29 Dec 2025.

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

- [Temporal Logics for Hyperproperties](https://mlsanity.com/paper/1401.4492/) (2014)
- [AutoHyper: Explicit-State Model Checking for HyperLTL](https://mlsanity.com/paper/2301.11229/) (2023)
- [Non-Deterministic Planning for Hyperproperty Verification](https://mlsanity.com/paper/2405.13488/) (2024)
- [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)
- [Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (extended version)](https://mlsanity.com/paper/2301.10037/) (2023)
- [Logics and Algorithms for Hyperproperties](https://mlsanity.com/paper/2501.08063/) (2025)
- [Prophecy Variables for Hyperproperty Verification](https://mlsanity.com/paper/2206.01797/) (2022)
- [Coinductive Proofs for Temporal Hyperliveness](https://mlsanity.com/paper/2501.07920/) (2025)
- [Prophecies all the Way: Game-based Model-Checking for HyperQPTL beyond forall^*exists^*](https://mlsanity.com/paper/2504.08575/) (2025)
- [On Hyperproperty Verification, Quantifier Alternations, and Games under Partial Information](https://mlsanity.com/paper/2510.03942/) (2025)

## Abstract (arXiv)

We study the connection of two problems within the planning and verification community: Conformant planning and model-checking of hyperproperties. Conformant planning is the task of finding a sequential plan that achieves a given objective independent of non-deterministic action effects during the plan's execution. Hyperproperties are system properties that relate multiple execution traces of a system and, e.g., capture information-flow and fairness policies. In this paper, we show that model-checking of exists^*forall^* hyperproperties is closely related to the problem of computing a conformant plan. Firstly, we show that we can efficiently reduce a hyperproperty model-checking instance to a conformant planning instance, and prove that our encoding is sound and complete. Secondly, we establish the converse direction: Every conformant planning problem is, itself, a hyperproperty model-checking task.