Strategy logic

Strategy Logic (SL) is a family of temporal logics used in formal verification, game theory, and multi-agent systems to reason explicitly about the strategies available to agents. Unlike formalisms such as alternating-time temporal logic (ATL and ATL*), in which strategic ability is primarily expressed through modalities for agents or coalitions, Strategy Logic allows strategies themselves to be quantified as logical objects. In modern formulations, strategy variables can also be explicitly bound to individual agents.

The original form of Strategy Logic was introduced by Krishnendu Chatterjee, Thomas A. Henzinger, and Nir Piterman at the 2007 International Conference on Concurrency Theory (CONCUR). The work was subsequently developed into a journal article published in Information and Computation in 2010. The CONCUR paper received a CONCUR Test-of-Time Award in 2026.

Background and development

Alternating-time temporal logic (ATL and ATL*) allows reasoning about what agents or coalitions can achieve, but does not treat strategies themselves as explicit objects. Strategy Logic extended this approach by allowing direct quantification over strategies, which allows reasoning about game-theoretic solutions such as Nash equilibrium.

CHP-SL

The original Strategy Logic was introduced by Krishnendu Chatterjee, Thomas A. Henzinger, and Nir Piterman in 2007 and developed further in 2010. Later literature refers to it as CHP-SL to distinguish it from a subsequent generalization. CHP-SL is defined for two-player turn-based games and uses first-order quantification over strategies.

Generalized Strategy Logic

Fabio Mogavero, Aniello Murano, and Moshe Y. Vardi generalized the logic in 2010 to multi-agent concurrent games. In this formulation, usually denoted simply SL, strategies are not tied to particular agents; an explicit binding operator assigns a strategy to an agent, allowing strategies to be shared or reused. SL strictly includes CHP-SL.

The generalized logic was developed further by Mogavero, Murano, Giuseppe Perelli, and Vardi in 2014, including results on model checking and several syntactic fragments. The remainder of this article uses SL to refer to this generalized formulation, which has been widely adopted by the community.

Formalism

Strategy Logic is normally interpreted over game-based models such as labelled game graphs or concurrent game structures. A strategy specifies how an agent should act as a game develops, potentially depending on the finite history of states or actions observed so far.

In the multi-agent formulation of Strategy Logic, formulas combine temporal operators with two principal mechanisms:

• strategy quantification, which existentially or universally quantifies over possible strategies; and
• agent binding, which associates a selected strategy with a particular agent.

After strategies have been selected and bound to the relevant agents, temporal formulas can describe properties of the plays produced by those choices. This separation between quantifying a strategy and assigning it to an agent distinguishes Strategy Logic from strategic modal logics in which strategy selection is incorporated directly into a coalition operator.

Syntax

Informally, Strategy Logic can be viewed as first-order logic quantification over strategies with temporal properties specified in linear temporal logic. The set of well-formed SL formulas can be defined by the following BNF-style grammar:

$${\displaystyle \varphi$$ ::=p\mid \neg \varphi \mid \varphi \land \varphi \mid \varphi \lor \varphi \mid {\mathsf {X}}\varphi \mid \varphi \,{\mathsf {U}}\,\varphi \mid \varphi \,{\mathsf {R}}\,\varphi \mid \langle \!\langle x\rangle \!\rangle \varphi \mid [\![x]\!]\varphi \mid (a,x)\varphi }

where $p\in AP$ is an atomic proposition, $x\in Var$ is a strategy variable, and $a\in Ag$ is an agent. The operators ${\mathsf {X}}$, ${\mathsf {U}}$, and ${\mathsf {R}}$ are respectively the LTL next, until, and release operators. The strategy quantifiers $\langle \langle x\rangle \rangle$ and $[[x]]$ respectively quantify existentially and universally over strategies, while $(a,x)$ binds agent $a$ to the strategy represented by $x$.

The usual temporal operators eventually and globally may be introduced as abbreviations: ${\mathsf {F}}\varphi \equiv {\mathsf {true}}{\mathsf {U}}\varphi$ and ${\mathsf {G}}\varphi \equiv {\mathsf {false}}{\mathsf {R}}\varphi$.

Expressive power

The explicit treatment of strategies gives Strategy Logic greater expressive power than several earlier strategic temporal logics. The original formulation showed that a fragment with a limited alternation of strategy quantifiers can express the existence of Nash equilibria and secure equilibria. In its original setting, it also subsumes ATL, ATL*, and game logic.

The later multi-agent formulation of Strategy Logic also subsumes ATL* and enables formulas in which strategic choices can be compared, shared, reused, or made dependent on other quantified strategies. These capabilities have made Strategy Logic a framework for studying formal notions of rational behaviour as well as the verification of multi-agent systems.

Model checking and satisfiability

The expressiveness of Strategy Logic results in high computational complexity. The model-checking problem for the full multi-agent logic is decidable but has non-elementary complexity. The satisfiability problem for unrestricted Strategy Logic is highly undecidable.

Researchers have therefore studied fragments of the logic that retain substantial expressive power while having more manageable decision problems. One of the best-known is One-Goal Strategy Logic (SL[1G]), a syntactic fragment introduced by Mogavero, Murano, Perelli, and Vardi in 2012. It restricts each strategic quantification to a single temporal goal. SL[1G] strictly subsumes ATL* while retaining decidable satisfiability, which is 2-EXPTIME-complete.

Automata-based procedures have also been developed for verification and synthesis from SL[1G] specifications. Petr Čermák, Alessio Lomuscio, and Aniello Murano presented a symbolic, binary decision diagram-based model-checking approach for the fragment and evaluated it on multi-agent-system examples. Work on the semantics and computational properties of the logic has continued. For example, research on strategy dependencies has examined how existentially quantified strategies may depend on strategies selected earlier in a formula and has proposed alternative forms of dependence for large fragments of Strategy Logic.

Extensions

Several extensions and variants of Strategy Logic have been developed to model additional features of strategic interaction. These include versions dealing with imperfect information, probabilistic behaviour, epistemic reasoning, and graded quantification over strategies.

Strategy Logic with imperfect information studies situations in which agents do not necessarily have complete knowledge of the state of a game. This setting substantially affects decidability and model-checking results.

Recognition and influence

Following its introduction, Strategy Logic became the basis of a substantial body of research on strategic reasoning, including work on model checking, satisfiability, strategy dependence, imperfect information, probabilistic systems, and formal verification of multi-agent systems. Strategy Logic has also been applied to the verification of multi-agent systems in which actions are publicly observable. Work in this area has considered extensions capable of expressing properties including Nash equilibria, Pareto optimality, and evolutionary stability.

In 2026, the original 2007 paper by Chatterjee, Henzinger, and Piterman was selected for a CONCUR Test-of-Time Award, recognising its long-term influence on research in concurrency theory and strategic reasoning.

See also

• Alternating-time temporal logic
• Linear temporal logic
• Temporal logic
• Model checking
• Formal verification
• Multi-agent system
• Game theory
• Nash equilibrium