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
χ	U+03C7	Chi	Assignment of strategies to agents
∃	U+2203	Existential quantifier	Reading of the strategy quantifier
∀	U+2200	Universal quantifier	Reading of the dual quantifier
∧	U+2227	Conjunction	Joins the clauses of the equilibrium formula
¬	U+00AC	Negation	No profitable deviation exists
φ, ψ	U+03C6, U+03C8	Phi, psi	Goals in the scope of a binding
x, y, z	—	Strategy variables	Bound by the strategy quantifiers
a, b, c	—	Agent variables	Range over the agent set
Ag	—	Agents	Set of agents
Str	—	Strategies	Strategy set

Metatheory. Chatterjee, Henzinger, and Piterman (2007, 2010) proved model checking decidable for their two-player Strategy Logic; Mogavero, Murano, and Vardi lifted the logic to multi-agent concurrent game structures and Mogavero, Murano, Perelli, and Vardi established the complexity: model checking full SL is decidable but non-elementary, while satisfiability is undecidable. The one-goal fragment SL[1G], in which each strategy quantifier prefix is followed by a single binding and goal, is 2EXPTIME-complete for model checking — the same cost as ATL* — and this is not accidental: SL[1G] admits a behavioural semantics, in which a quantified strategy may be chosen step by step on the basis of the history alone, so the automata construction stays within two exponentials. Full SL does not, since a quantified strategy there may depend on strategies quantified later, and this failure of behaviourality is the source of the tower. SL is strictly more expressive than ATL*: Nash equilibrium and dominance are definable in it and not in ATL*.

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

Limitations. The expressiveness that lets SL define equilibrium has two consequences: satisfiability is undecidable, so the logic cannot be used for synthesis from specification alone, and model checking is non-elementary, so no algorithm for the full language has a bound expressible as a fixed tower. The fragments that recover elementary complexity do so by forbidding the nesting that made equilibrium expressible in the first place. Semantics is over perfect-information concurrent game structures with perfect recall; imperfect information makes model checking undecidable, as it does for ATL. Strategies quantified over are arbitrary functions from histories to actions, with no bound on memory and no notion of cost, and the logic has no probabilities, so mixed strategies and the equilibria that require them fall outside it.