# Reasoning about Strategies: on the Satisfiability Problem

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 25 Nov 2016.

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

- [Human-Artificial Interaction in the Age of Agentic AI: A System-Theoretical Approach](https://mlsanity.com/paper/2502.14000/) (2025)
- [A Logic for Conditional Local Strategic Reasoning](https://mlsanity.com/paper/2102.06148/) (2021)
- [The Alternating-Time μ-Calculus With Disjunctive Explicit Strategies](https://mlsanity.com/paper/2305.18795/) (2023)

## Abstract (arXiv)

Strategy Logic (SL, for short) has been introduced by Mogavero, Murano, and Vardi as a useful formalism for reasoning explicitly about strategies, as first-order objects, in multi-agent concurrent games. This logic turns out to be very powerful, subsuming all major previously studied modal logics for strategic reasoning, including ATL, ATL*, and the like. Unfortunately, due to its high expressiveness, SL has a non-elementarily decidable model-checking problem and the satisfiability question is undecidable, specifically Sigma_1^1. In order to obtain a decidable sublogic, we introduce and study here One-Goal Strategy Logic (SL[1G], for short). This is a syntactic fragment of SL, strictly subsuming ATL*, which encompasses formulas in prenex normal form having a single temporal goal at a time, for every strategy quantification of agents. We prove that, unlike SL, SL[1G] has the bounded tree-model property and its satisfiability problem is decidable in 2ExpTime, thus not harder than the one for ATL*.