# Temporal Logics for Hyperproperties

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

## Key facts

- Cited by 19 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 17 Jan 2014.

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

- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [A Hazard Analysis Framework for Code Synthesis Large Language Models](https://mlsanity.com/paper/2207.14157/) (2022)
- [Generating Symbolic Reasoning Problems with Transformer GANs](https://mlsanity.com/paper/2110.10054/) (2021)
- [Non-Deterministic Planning for Hyperproperty Verification](https://mlsanity.com/paper/2405.13488/) (2024)
- [On Alternating-Time Temporal Logic, Hyperproperties, and Strategy Sharing](https://mlsanity.com/paper/2312.12403/) (2023)
- [HypRL: Reinforcement Learning of Control Policies for Hyperproperties](https://mlsanity.com/paper/2504.04675/) (2025)
- [Counterfactuals Modulo Temporal Logics](https://mlsanity.com/paper/2306.08916/) (2023)
- [Deductive Controller Synthesis for Probabilistic Hyperproperties](https://mlsanity.com/paper/2307.04503/) (2023)
- [Software Doping Analysis for Human Oversight](https://mlsanity.com/paper/2308.06186/) (2023)
- [Hyper Strategy Logic](https://mlsanity.com/paper/2403.13741/) (2024)
- [Bayesian Statistical Model Checking for Multi-agent Systems using HyperPCTL*](https://mlsanity.com/paper/2209.02672/) (2022)
- [On Quantified Observability Analysis in Multiagent Systems](https://mlsanity.com/paper/2310.02614/) (2023)
- [Monitoring Second-Order Hyperproperties](https://mlsanity.com/paper/2404.09652/) (2024)
- [Decentralized Planning Using Probabilistic Hyperproperties](https://mlsanity.com/paper/2502.13621/) (2025)
- [An Information-Flow Perspective on Explainability Requirements: Specification and Verification](https://mlsanity.com/paper/2509.01479/) (2025)
- [Strategy Logic, Imperfect Information, and Hyperproperties](https://mlsanity.com/paper/2510.03952/) (2025)
- [On Conformant Planning and Model-Checking of exists^*forall^* Hyperproperties](https://mlsanity.com/paper/2512.23324/) (2025)
- [Sample-Efficient Learning of Probabilistic Causes for Reachability in Markov Decision Processes with Probabilistic Guarantees](https://mlsanity.com/paper/2606.29681/) (2026)
- [HyPOLE: Hyperproperty-Guided Multi-Agent Reinforcement Learning under Partial Observation](https://mlsanity.com/paper/2606.30966/) (2026)

## Abstract (arXiv)

Two new logics for verification of hyperproperties are proposed. Hyperproperties characterize security policies, such as noninterference, as a property of sets of computation paths. Standard temporal logics such as LTL, CTL, and CTL* can refer only to a single path at a time, hence cannot express many hyperproperties of interest. The logics proposed here, HyperLTL and HyperCTL*, add explicit and simultaneous quantification over multiple paths to LTL and to CTL*. This kind of quantification enables expression of hyperproperties. A model checking algorithm for the proposed logics is given. For a fragment of HyperLTL, a prototype model checker has been implemented.