# On Alternating-Time Temporal Logic, Hyperproperties, and Strategy Sharing

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 8 of its 39 references that are in the map.
- First posted on arXiv 19 Dec 2023.

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

- [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)
- [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)
- [Oink: an Implementation and Evaluation of Modern Parity Game Solvers](https://mlsanity.com/paper/1801.03859/) (2018)
- [Reasoning about Quality and Fuzziness of Strategic Behaviours](https://mlsanity.com/paper/1905.11537/) (2019)
- [Multi-Valued Verification of Strategic Ability](https://mlsanity.com/paper/2310.20344/) (2023)

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

- [HypRL: Reinforcement Learning of Control Policies for Hyperproperties](https://mlsanity.com/paper/2504.04675/) (2025)
- [Strategy Logic, Imperfect Information, and Hyperproperties](https://mlsanity.com/paper/2510.03952/) (2025)

## Abstract (arXiv)

Alternating-time temporal logic (ATL^*) is a well-established framework for formal reasoning about multi-agent systems. However, while ATL^* can reason about the strategic ability of agents (e.g., some coalition A can ensure that a goal is reached eventually), we cannot compare multiple strategic interactions, nor can we require multiple agents to follow the same strategy. For example, we cannot state that coalition A can reach a goal sooner (or more often) than some other coalition A'. In this paper, we propose HyperATLS^*S, an extension of ATL^* in which we can (1) compare the outcome of multiple strategic interactions w.r.t. a hyperproperty, i.e., a property that refers to multiple paths at the same time, and (2) enforce that some agents share the same strategy. We show that HyperATL^*S is a rich specification language that captures important AI-related properties that were out of reach of existing logics. We prove that model checking of HyperATL^*S on concurrent game structures is decidable. We implement our model-checking algorithm in a tool we call HyMASMC and evaluate it on a range of benchmarks.