# Hyperproperties for Robotics: Planning via HyperLTL

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

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 26 Nov 2019.

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

- [Probabilistic Planning with Prioritized Preferences over Temporal Logic Objectives](https://mlsanity.com/paper/2304.11641/) (2023)
- [Deductive Controller Synthesis for Probabilistic Hyperproperties](https://mlsanity.com/paper/2307.04503/) (2023)
- [Bayesian Statistical Model Checking for Multi-agent Systems using HyperPCTL*](https://mlsanity.com/paper/2209.02672/) (2022)
- [Decentralized Planning Using Probabilistic Hyperproperties](https://mlsanity.com/paper/2502.13621/) (2025)
- [Multi-Agent Planning with Spatio-Temporal and Topological Constraints using STL-GO](https://mlsanity.com/paper/2607.28679/) (2026)

## Abstract (arXiv)

There is a growing interest on formal methods-based robotic planning for temporal logic objectives. In this work, we extend the scope of existing synthesis methods to hyper-temporal logics. We are motivated by the fact that important planning objectives, such as optimality, robustness, and privacy, (maybe implicitly) involve the interrelation between multiple paths. Such objectives are thus hyperproperties, and cannot be expressed with usual temporal logics like the linear temporal logic (LTL). We show that such hyperproperties can be expressed by HyperLTL, an extension of LTL to multiple paths. To handle the complexity of planning with HyperLTL specifications, we introduce a symbolic approach for synthesizing planning strategies on discrete transition systems. Our planning method is evaluated on several case studies.