# Strategy Logic

**Origin.** Krishnendu Chatterjee, Thomas Henzinger, and Nir Piterman introduced Strategy Logic (SL, 2007, 2010). Extends ATL with explicit strategy quantification. Strategies are first-class objects: quantify over them, bind them to agents. More expressive than ATL* but with higher complexity. Foundation for advanced multi-agent verification.

**Models.** Explicit strategy quantification. In ATL, ⟨⟨A⟩⟩φ implicitly asks if coalition A has a strategy. In SL, strategies are named: ⟨⟨x⟩⟩(a,x)φ means "there exists a strategy x such that when agent a uses x, φ holds." Can express: Nash equilibrium, strategy sharing, blame, and more.

**Formalism.**

*Syntax:*
- Agent variables: a, b, c, ... (∈ Ag)
- Strategy variables: x, y, z, ...
- ⟨⟨x⟩⟩φ — strategy quantifier: "there exists a strategy x"
- [[x]]φ — "for all strategies x"
- (a, x)φ — bind agent a to strategy x in φ
- Temporal: Xφ, Gφ, Fφ, φUψ

*Semantics:*
Evaluated on concurrent game structures with strategy assignment.
χ: Ag → Strategies maps agents to strategies.

*Key formulas:*
- ⟨⟨x⟩⟩(a,x) Fwin — agent a has a winning strategy
  (Like ⟨⟨{a}⟩⟩Fwin in ATL)
- ⟨⟨x⟩⟩(a,x)(b,x) Fwin — a and b share a strategy to win
- ⟨⟨x⟩⟩[[y]](a,x)(b,y) Fwin_a — a has a strategy winning against any b strategy
- Nash equilibrium:
  ⟨⟨x⟩⟩⟨⟨y⟩⟩[(a,x)(b,y) outcome ∧
    [[x']](a,x')(b,y)¬better_a ∧ [[y']](a,x)(b,y')¬better_b]

*Binding:*
(a, x) binds agent a to use strategy x.
Multiple agents can share: (a,x)(b,x).
Agents can change: (a,x)φ ∧ (a,y)ψ.

*Fragments:*
- SL[1G]: one-goal fragment (simpler, decidable)
- ATL* embeds: ⟨⟨A⟩⟩φ = ⟨⟨x⟩⟩(a₁,x)...(aₙ,x)φ where A = {a₁,...,aₙ}

**Symbols.**

| Symbol | Unicode | Name | Meaning |
|--------|---------|------|---------|
| ⟨⟨x⟩⟩ | — | Strategy exists | ∃ strategy x |
| [[x]] | — | Strategy forall | ∀ strategies x |
| (a, x) | — | Binding | Agent a uses strategy x |
| X | — | Next | Next state |
| G | — | Globally | Always |
| F | — | Finally | Eventually |
| U | — | Until | Until |
| Ag | — | Agents | Set of agents |
| Str | — | Strategies | Strategy set |

**Metatheory.** Full SL model checking is non-elementary (tower of exponentials). SL[1G] (one binding goal) is 2EXPTIME-complete. Satisfiability is undecidable for full SL. Strictly more expressive than ATL*: can express Nash equilibrium, which ATL* cannot. Bisimulation-invariant fragment equals μ-calculus over concurrent game structures.

**Applies to.** Game theory formalization (Nash equilibrium, dominance). Multi-agent system verification. Security (strategies against attackers). Mechanism design verification. Rational synthesis. Automated negotiation.

**Limitations.** Very high complexity — impractical for large systems without restrictions. Syntax is complex; formulas hard to write and read. Strategies are abstract; extracting concrete strategies is additional work. Limited tool support compared to simpler logics. Full SL has undecidable satisfiability.

© 2026 Lingenic LLC