wiki

Cooperative Reward Machine Synthesis

2 min read

Cooperative Reward Machine Synthesis

Context

Varricchione2023 - Synthesising Reward Machines for Cooperative MARL uses ATL specifications and strategy witnesses to synthesize team and individual reward machines for cooperative multi-agent reinforcement learning.

Formal Statement

A reward machine is written

where U is the RM state set, u_I is the initial RM state, Sigma is an event alphabet, t is the transition function, and r assigns transition rewards.

The input side consists of:

  • a multi-agent environment and labeling function;
  • an epistemic/concurrent game structure for strategic reasoning;
  • an ATL formula such as <<A>>phi specifying a team objective;
  • a uniform strategy witness for the coalition ability claim.

The synthesis procedure builds a coalitional reward machine from the event sequences compatible with the witness, then projects individual reward machines for decentralized learning.

Derivation / Construction

  • The ATL model checker supplies a strategy witness for the coalition task.
  • Event sequences observed along witness-consistent paths are converted into RM progress states.
  • The team RM encodes completion/failure of the cooperative task.
  • Individual projected RMs give each agent a local progress signal compatible with decentralized Q-learning.
  • Theorem-level guarantees relate the probability of individual subtask completion to coalition task completion/failure under the learned policies.

Implications

  • Strategic task specifications can be compiled into learning-facing reward structure.
  • Synthesis reduces manual reward-machine design in cooperative MARL.
  • Because ATL can express constraints on coalition strategies, it can carry specification-level safety or coordination constraints into the reward-machine layer.

Graph View

Backlinks