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](b,y) Fwin_a — a has a strategy winning against any b strategy
Nash equilibrium: ⟨⟨x⟩⟩⟨⟨y⟩⟩[(a,x)(b,y) outcome ∧ [x'](b,y)¬better_a ∧ [y'](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.