# Hyper Strategy Logic

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 16 of its 53 references that are in the map.
- First posted on arXiv 20 Mar 2024.

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

- [From Spot 2.0 to Spot 2.10: What's New?](https://mlsanity.com/paper/2206.11366/) (2022)
- [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)
- [Strategy Logic with Imperfect Information](https://mlsanity.com/paper/1805.12592/) (2018)
- [Decidability results for ATL* with imperfect information and perfect recall](https://mlsanity.com/paper/1805.12582/) (2018)
- [A Temporal Logic for Strategic Hyperproperties](https://mlsanity.com/paper/2107.02509/) (2021)
- [Unifying Hyper and Epistemic Temporal Logic](https://mlsanity.com/paper/1409.2711/) (2014)
- [Reasoning about Quality and Fuzziness of Strategic Behaviours](https://mlsanity.com/paper/1905.11537/) (2019)
- [The Hierarchy of Hyperlogics](https://mlsanity.com/paper/2005.05934/) (2020)
- [Opacity of nondeterministic transition systems: A (bi)simulation relation approach](https://mlsanity.com/paper/1802.03321/) (2018)
- [Synthesizing Reactive Systems from Hyperproperties](https://mlsanity.com/paper/1905.13511/) (2019)
- [Dealing with imperfect information in Strategy Logic](https://mlsanity.com/paper/1908.02488/) (2019)
- [Propositional Dynamic Logic for Hyperproperties](https://mlsanity.com/paper/1910.10546/) (2019)
- [ATLsc with partial observation](https://mlsanity.com/paper/1509.07208/) (2015)
- [The First-Order Logic of Hyperproperties](https://mlsanity.com/paper/1610.04388/) (2016)
- [Scalable Verification of Strategy Logic through Three-valued Abstraction](https://mlsanity.com/paper/2310.17219/) (2023)

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

- [HypRL: Reinforcement Learning of Control Policies for Hyperproperties](https://mlsanity.com/paper/2504.04675/) (2025)

## Abstract (arXiv)

Strategy logic (SL) is a powerful temporal logic that enables strategic reasoning in multi-agent systems. SL supports explicit (first-order) quantification over strategies and provides a logical framework to express many important properties such as Nash equilibria, dominant strategies, etc. While in SL the same strategy can be used in multiple strategy profiles, each such profile is evaluated w.r.t. a path-property, i.e., a property that considers the single path resulting from a particular strategic interaction. In this paper, we present Hyper Strategy Logic (HyperSL), a strategy logic where the outcome of multiple strategy profiles can be compared w.r.t. a hyperproperty, i.e., a property that relates multiple paths. We show that HyperSL can capture important properties that cannot be expressed in SL, including non-interference, quantitative Nash equilibria, optimal adversarial planning, and reasoning under imperfect information. On the algorithmic side, we identify an expressive fragment of HyperSL with decidable model checking and present a model-checking algorithm. We contribute a prototype implementation of our algorithm and report on encouraging experimental results.