Research map / Multi-agent systems and games / Games and equilibria
On Alternating-Time Temporal Logic, Hyperproperties, and Strategy Sharing
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Proposes HyperATL*_S, extending ATL* with path variables (hyperproperties) and strategy-sharing constraints, proves decidability of model checking via alternating parity automata, and implements it in the HyMASMC tool evaluated on ISPL benchmarks.
Problem
ATL* can only reason about a single path in isolation, so it cannot compare multiple strategic interactions (hyperproperties) or require several agents to follow the same strategy.
Approach
Extend HyperATL* with a sharing constraint on strategy quantifiers so agents can be forced to play the same strategy, and give a model-checking algorithm that eliminates path quantifiers incrementally using alternating parity automata over zipped path assignments, simulating the game inside the automaton.
Key results
- On the ATL* scheduler benchmark, HyMASMC verifies n=5 (|S|=15552) in 347.1 s where MCMAS-SL[1G] times out at 1h; for n=4 HyMASMC takes 24.3 s vs 322.7 s for MCMAS-SL[1G].
- HyMASMC verifies almost all sampled hyperproperty instances (optimality, observational determinism, good-enough synthesis) across ISPL models within a few seconds on average.
- The software-development model (about 15k states) is too large for HyMASMC's automata-based approach and yields no results.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Use HyMASMC instead of MCMAS-SL[1G] | ATL* scheduling verification · Scheduling, n=2 | verification time: 0.11 -> 0.41 | Hurt |
| Use HyMASMC instead of MCMAS-SL[1G] | ATL* scheduling verification · Scheduling, n=3 | verification time: 6.64 -> 2.06 | Helped |
| Use HyMASMC instead of MCMAS-SL[1G] | ATL* scheduling verification · Scheduling, n=4 | verification time: 322.7 -> 24.3 | Helped |
| Use HyMASMC instead of MCMAS-SL[1G] | ATL* scheduling verification · Scheduling, n=5 | verification time: TO -> 347.1 | Helped |
Surprising findings
- The software-development model (about 15k states) could not be handled by HyMASMC, and MCMAS-SL[1G] cannot verify even simple ATL* specifications on it.
Limitations
- Model checking has non-elementary worst-case complexity, with 2m-EXPTIME for nesting-rank m.
- Automata-based approach does not scale to large models such as software-development (~15k states).
- Properties were evaluated on sampled instances from ISPL models and not on real-world scenarios.
Experimental setup
Datasets: ISPL models from MCMAS benchmarks (bit-transmission, book-store, card-game, dining cryptographers, muddy-children, simpl
Benchmarks: ISPL models from MCMAS parametric scheduler benchmark
Metrics: verification time (seconds)
Baselines: MCMAS-SL[1G]
Builds on: ATL* HyperATL* HyperLTL strategy logic
Closest papers by meaning
- A Modal Logic for Joint Abilities of Structured Strategies with Bounded Complexity (AAAI 2025 · similarity 0.88)
- Natural Strategic Ability in Stochastic Multi-Agent Systems (AAAI 2024 · similarity 0.88)
- Responsibility-aware Strategic Reasoning in Probabilistic Multi-Agent Systems (AAAI 2025 · similarity 0.88)
- Strat-Reasoner: Reinforcing Strategic Reasoning of LLMs in Multi-Agent Games (ICML 2026 · similarity 0.85)
- GTBench: Uncovering the Strategic Reasoning Capabilities of LLMs via Game-Theoretic Evaluations (NeurIPS 2024 · similarity 0.85)
- Sparks of Cooperative Reasoning: LLMs as Strategic Hanabi Agents (ICML 2026 · similarity 0.85)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.