# The Complexity of Monitoring Hyperproperties

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

## Key facts

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

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

- [HypRL: Reinforcement Learning of Control Policies for Hyperproperties](https://mlsanity.com/paper/2504.04675/) (2025)
- [On Quantified Observability Analysis in Multiagent Systems](https://mlsanity.com/paper/2310.02614/) (2023)
- [The Oversight Gap: What LLM Safety Monitors Miss, and Why It Is Not Capability](https://mlsanity.com/paper/2609.07162/) (2026)

## Abstract (arXiv)

We study the runtime verification of hyperproperties, expressed in the temporal logic HyperLTL, as a means to inspect a system with respect to security polices. Runtime monitors for hyperproperties analyze trace logs that are organized by common prefixes in the form of a tree-shaped Kripke structure, or are organized both by common prefixes and by common suffixes in the form of an acyclic Kripke structure. Unlike runtime verification techniques for trace properties, where the monitor tracks the state of the specification but usually does not need to store traces, a monitor for hyperproperties repeatedly model checks the growing Kripke structure. This calls for a rigorous complexity analysis of the model checking problem over tree-shaped and acyclic Kripke structures. We show that for trees, the complexity in the size of the Kripke structure is L-complete independently of the number of quantifier alternations in the HyperLTL formula. For acyclic Kripke structures, the complexity is PSPACE-complete (in the level of the polynomial hierarchy that corresponds to the number of quantifier alternations). The combined complexity in the size of the Kripke structure and the length of the HyperLTL formula is PSPACE-complete for both trees and acyclic Kripke structures, and is as low as NC for the relevant case of trees and alternation-free HyperLTL formulas. Thus, the size and shape of both the Kripke structure and the formula have significant impact on the complexity of the model checking problem.