Source-linked AI summary
SpecMAGIC: Specification-Guided Multi-Task Generalization in Multi-Agent Reinforcement Learning
Zijian Guo, İlker Işık, H. M. Sabbir Ahmad, Wenchao Li
TL;DR
Zero-shot generalization across temporally extended multi-agent tasks with changing coordination requirements remains underexplored. SpecMAGIC combines a coordination-aware specification language, centralized subtask planning, and decentralized policies. It reports improved generalization on unseen specifications and strong performance as agent numbers increase.
Problem
Zero-shot generalization to complex, temporally extended multi-agent tasks with diverse coordination requirements remains underexplored, although such tasks arise in real-world applications.
Source: §1 · p. 1Method
SpecMAGIC adds dependency and count operators to task specifications, plans centrally over compatible reach-avoid subtask sequences, and executes them with reusable decentralized policies.
Source: §1 · p. 2, §4.4 · p. 6Results
Takeaways & Limitations
The framework supports reuse of learned subtask policies across unseen finite- and infinite-horizon specifications without retraining.
Source: §1 · p. 2, §4.4 · p. 6, §6 · p. 9The high-level planner remains centralized, which may limit scalability as the number of agents further increases.
Source: §6 · p. 9
Abstract
from arXiv · showhide
Multi-task generalization is an important yet underexplored problem in multi-agent reinforcement learning (MARL). Many real-world applications require multi-agent systems to generalize across complex, temporally extended tasks with diverse inter-agent coordination requirements. We introduce a specification language that combines temporal-logic task specifications with operators for expressing such requirements. We propose SpecMAGIC, a hierarchical framework that leverages the automaton structure of task specifications for subtask decomposition. A centralized high-level planner identifies and allocates compatible subtask sequences across agents, while decentralized low-level policies execute individual subtasks. This enables zero-shot generalization to new tasks by composing reusable subtask policies according to new specifications, without retraining. We establish soundness and probabilistic completeness of the high-level planner. Experiments on multi-agent navigation tasks show that SpecMAGIC substantially outperforms existing approaches on unseen task specifications and maintains strong performance as the number of agents increases.
1 INTRODUCTION
Zero-shot generalization to temporally extended multi-agent tasks with changing coordination requirements remains underexplored. SpecMAGIC combines coordination-aware specifications with hierarchical planning and reusable subtask policies.
1 INTRODUCTION
- Zero-shot generalization remains underexplored when complex, temporally extended multi-agent tasks have diverse coordination requirements that can change at test time.Both individual tasks and the coordination structure among agents may differ from training.Source: §1 · p. 1
- SpecMAGIC introduces dependency and count operators and decomposes specifications into reach-avoid subtasks for planning without constructing a global automaton.A centralized sampling-based planner allocates compatible subtasks across agents for decentralized subtask-conditioned policies to execute.Source: §1 · p. 2
- The planner avoids the exponential complexity of explicit global product-automaton construction and has soundness and probabilistic-completeness guarantees.The guarantees mean returned plans satisfy the specification, and feasible plans are found with probability approaching one as sampling iterations increase.Source: §1 · p. 2
- Experiments across navigation specifications and agent counts show consistent zero-shot improvements over state-of-the-art baselines and scalability.The introduction reports diverse specifications and varying numbers of agents, without giving numerical results here.Source: §1 · p. 2
2 RELATED WORK
Prior work studies specification-driven learning, multi-agent planning, and task allocation, but the paper targets zero-shot generalization across unseen specifications with explicit coordination requirements.
2 RELATED WORK
- Specification-driven RL has studied unseen tasks through direct specification or automaton encoding and through subtask decomposition.In multi-agent work, formal specifications guide global coordination, while MTMARL studies also consider collections of tasks.Source: §2 · p. 2
- ACC-MARL considers unseen specifications but is limited to finite-horizon single-agent tasks, unlike this paper’s finite- and infinite-horizon tasks with explicit inter-agent coordination.The passage identifies ACC-MARL as the closest work.Source: §2 · p. 2
- Existing multi-agent temporal-logic allocation methods typically plan for a given specification, while hierarchical MTMARL methods do not consider temporal-logic specifications.This paper’s planner samples reach-avoid subtask sequences and avoids constructing the global product automaton.Source: §2 · p. 2
3 PRELIMINARIES
The preliminaries define a partially observable multi-agent setting and use LTL and Büchi automata to represent temporal tasks and progress toward their satisfaction.
3 PRELIMINARIES
- A partially observable Markov game specifies joint states, actions, transitions, observations, and local policies, with task rewards induced by the specification at test time.Each agent acts from its local observation; the formulation does not explicitly include a reward function.Source: §3 · p. 3
- LTL formulas express temporal properties using Boolean operators and the temporal operators until, eventually, and always.A trajectory satisfies a formula when its proposition trace satisfies that formula.Source: §3 · p. 3
- Büchi automata represent LTL specifications, and reach-avoid subtasks encode progress toward satisfaction while identifying transitions that can lead to violation.The reach condition corresponds to progress along an accepting run; the avoid condition captures transitions outside such a run.Source: §3 · p. 3
4 METHOD
SpecMAGIC represents individual tasks and coordination requirements as specification components, plans over reach-avoid subtask sequences, and uses decentralized policies to execute planned subtasks.
4.1 PROBLEM STATEMENT
- The framework combines individual-agent specifications with inter-agent dependency and count requirements in a global specification.Its method comprises a centralized sampling-based planner and decentralized subtask-conditioned policies.Source: §4.1 · p. 3, §4 · p. 3, Figure 1 · p. 4
4.2 SPECIFICATION LANGUAGE
- The specification language augments individual-agent LTL formulas with operators for dependency and count requirements.The language describes coordination constraints and gives examples from surveillance, warehouse automation, and manufacturing.Source: §4.2 · p. 4
4.3 TASK DECOMPOSITION AND ALLOCATION
- The planner searches over component reach-avoid sequences to find compatible combinations without explicitly constructing the global product automaton.It samples expandable components and candidate sequences, incrementally building a tree over subtask progress; every component’s avoid condition is retained when checking compatibility.Source: §4.3 · pp. 5–6
- Any path returned by the planner satisfies the global specification, and if a feasible sequence exists, the probability of finding one approaches one with more sampling iterations.The latter guarantee is probabilistic completeness.Source: §4.3 · p. 6
4.4 POLICY LEARNING
- Decentralized policies take each agent’s local observation and current reach-avoid subtask as input, and are trained on independently sampled subtasks.The centralized planner handles high-level ordering or synchronization at test time, where learned policies are reused across unseen specifications without retraining.Source: §4.4 · p. 6
5 EXPERIMENTS
Experiments in the Zone navigation environment evaluate zero-shot generalization, scaling across agent counts, and the sampling-based planner against a product-automaton search planner.
5.1 CAN SPECMAGIC GENERALIZE ZERO-SHOT TO UNSEEN TASK SPECIFICATIONS (Q1)?
- SpecMAGIC consistently outperforms ACC-MARL across evaluated finite-horizon specifications in success, violations, and steps, including unseen tasks.Performance generally declines as specification complexity increases, but remains strong on more complex and OOD specifications.Source: Table 1 · p. 7, §5.1 · p. 8
- The method also handles infinite-horizon specifications, but ACC-MARL is excluded because its DFA-based approach cannot represent them.Results are reported for SpecMAGIC alone as a reference for future comparisons.Source: §5.1 · p. 8
5.2 HOW WELL DOES SPECMAGIC SCALE AS THE NUMBER OF AGENTS INCREASES? (Q2)
- As agent counts grow, global automata become intractable to construct at 10 agents, while the sampling planner's tree size and iterations increase moderately.The reported planning time excludes automaton-construction time.Source: §5.2 · p. 8, Table 2 · p. 8
- Without retraining, policies transfer across agent counts; performance tends to drop when evaluation uses more agents than training, while training with more agents generally helps.For fewer evaluation agents, policies trained with more agents maintain or slightly improve performance.Source: §5.2 · pp. 8–9, Figure 3 · p. 9
5.3 ABLATION STUDY: WHAT IS THE IMPACT OF THE PROPOSED SAMPLING-BASED PLANNER ON SPECMAGIC VERSUS A REFERENCE SEARCH-BASED PLANNER? (Q3)
- The sampling-based planner matches the search-based planner on success, violations, and steps while requiring substantially less planning time, especially for more complex specifications.The comparison covers three-agent IND specifications; search failed to find a feasible path within 10 minutes for specifications involving four or more agents.Source: §5.3 · p. 9, Figure 4 · p. 9
6 CONCLUSION AND FUTURE WORK
The conclusion presents SpecMAGIC as a zero-shot framework for diverse LTL specifications, while identifying centralized planning as a possible scalability constraint.
6 CONCLUSION AND FUTURE WORK
- SpecMAGIC combines a centralized sampling-based planner over reach-avoid subtasks with decentralized subtask-conditioned policies for low-level execution.The planner has soundness and probabilistic completeness guarantees.Source: §6 · p. 9
- Experiments show strong generalization across finite- and infinite-horizon specifications and continued effectiveness as agent numbers increase.Source: §6 · p. 9
- The centralized high-level planner may limit scalability as the number of agents increases; future work will investigate fully decentralized planning.The authors also propose integrating alternative safe RL methods into low-level policies to better handle safety constraints.Source: §6 · p. 9
AI USE STATEMENT
The statements report AI-assisted work and author review, caution about task-specification safety, and identify supplementary reproducibility materials.
AI USE STATEMENT
- Generative AI supported grammar checking and parts of the code, which two authors reviewed, verified, and tested.The authors take responsibility for the final work, including AI-assisted text, claims, and artifacts.Source: AI USE STATEMENT · p. 10
ETHICS STATEMENT
- Task specifications should be designed carefully to avoid unsafe or undesirable behaviors.Source: ETHICS STATEMENT · p. 10
REPRODUCIBILITY STATEMENT
- Source code and implementation details needed to reproduce the reported experiments and results are provided in supplementary materials.Source: REPRODUCIBILITY STATEMENT · p. 10
A THEORETICAL ANALYSIS
The planner is proven sound, and probabilistically complete when a feasible subtask sequence exists. The described Zone environments use 3, 5, or 10 agents with episode-randomized agent and zone positions.
A THEORETICAL ANALYSIS
- Every path returned by the sampling-based planner is an accepting path satisfying the global specification.The proof follows from preserving subtask order and compatibility along the returned path.Source: A THEORETICAL ANALYSIS · p. 13
- If a feasible subtask sequence exists, the probability that the planner finds one converges to one as sampling iterations increase.The proof uses a positive lower bound on the probability of each successful extension.Source: A THEORETICAL ANALYSIS · p. 13
B.1 ENVIRONMENTS
- Zone environments evaluate 3-, 5-, and 10-agent settings, with agent and zone positions randomly sampled each episode.The 10-agent environment is slightly larger, with larger colored regions.Source: §B.1 · p. 14, Figure 5 · p. 14
B.2 SPECIFICATIONS
The evaluation spans task specifications with individual goals, inter-agent dependencies, and count constraints, including structurally more complex out-of-distribution cases. The section also reports that sampling is more practical than search for complex global specifications with large automata.
B.2 SPECIFICATIONS
- The evaluation covers four task classes combining individual specifications with dependency requirements, count constraints, or both.The OOD specifications have longer temporal dependencies and more compositional constraints than those encountered during training.Source: §B.2 · p. 14, Table 3 · p. 15
- Scalability tests vary training and evaluation teams across 3, 5, and 10 agents while constructing constraints involving every agent.The tests combine individual, dependency, and count specifications.Source: §B.2 · p. 14
- Sampling is more practical than search for complex global specifications with large automata.The compared global automata average 99.67 ± 34.72 states and 1851.00 ± 908.17 transitions, versus 6.53 ± 3.30 states and 21.47 ± 19.23 transitions for individual specifications.Source: §B.2 · pp. 14–15
- Dependency and count operators compactly express inter-agent requirements and translate compositionally into standard LTL without extending its expressiveness.The operators encode prerequisites between propositions and synchronous or asynchronous requirements on how many agents satisfy a proposition.Source: §B.2 · p. 15
C IMPLEMENTATION DETAILS
The implementation trains decentralized low-level policies on reach-avoid subtasks and uses a centralized planner to compose compatible subtask sequences. It also specifies the training setup, compatibility checks, replanning procedure, and evaluation measures.
C IMPLEMENTATION DETAILS
- The implementation adapts GenZ-LTL to multiple agents and trains methods for 15M environment interactions using common network architectures.The actor and critic have three hidden layers of size [64, 64, 64], and the value-function network has two hidden layers of size [64, 64].Source: C IMPLEMENTATION DETAILS · p. 16
- Low-level policies are trained on sampled reach-avoid subtasks, with reach satisfaction rewarded and avoid satisfaction or collision penalized.The policy and critics are shared across homogeneous agents; an episode terminates if any agent incurs a cost.Source: C IMPLEMENTATION DETAILS · p. 16
- Finite-horizon success requires every specification component to be satisfied, while violation occurs if any component is violated.For 10-agent specifications, complete product automata exceeded a one-hour construction limit, so the reported state count is a lower bound.Source: C IMPLEMENTATION DETAILS · p. 16
- The sampling planner searches over feasible subtask sequences, extending nodes by sampling components and checking selected subtasks for compatibility.Each node records the selected sequence and current subtask for each specification component.Source: C IMPLEMENTATION DETAILS · pp. 16–17
- Reach-avoid compatibility is checked from Boolean clauses: a reach clause contained in an avoid clause makes the conditions incompatible.Otherwise, propositions already in the reach condition are removed from avoid clauses.Source: C IMPLEMENTATION DETAILS · p. 17
- When an automaton state changes, the planner recomputes feasible subtask sequences and replans from current specification progress.For infinite-horizon tasks, candidate sequences use a finite prefix followed by repeated cyclic suffixes; value-guided lookahead is left for future work.Source: C IMPLEMENTATION DETAILS · p. 17
D ADDITIONAL RESULTS
Additional evaluations examine simple and infinite-horizon tasks, then vary coordination-specification complexity. The results describe performance across these settings and the planning-time behavior as coordination requirements grow.
Performance on simple specifications
- SpecMAGIC maintains consistently high success and low violation rates on simple and complex specifications, while ACC-MARL performs substantially better on the simple specifications than on the complex main experiments.For reach-only tasks, violations arise solely from inter-agent collisions; the authors suggest ACC-MARL’s degradation is mainly due to increased specification complexity.Source: D ADDITIONAL RESULTS · p. 17, Table 4 · p. 18
Infinite-horizon tasks
- On evaluated infinite-horizon G F φ tasks, SpecMAGIC obtains low violation rates and frequent accepting-state visits, with slightly higher violations and fewer visits as coordination requirements are introduced.The evaluation has no baseline comparison because ACC-MARL’s DFAs cannot represent infinite-horizon specifications; the same sampling-based planner can be repeatedly applied to subtask sequences.Source: D ADDITIONAL RESULTS · p. 18, Table 5 · p. 18
Coordination-specification complexity
- As dependency or count requirements increase, success generally falls while violations and steps to satisfaction rise; planning time remains tractable.Each agent has a simple reach-only task, and the two coordination-operator types are varied separately; the planner works directly on subtask sequences without constructing the product automaton.Source: D ADDITIONAL RESULTS · pp. 18–19, Figure 6 · p. 18
E QUALITATIVE RESULTS
A three-agent example illustrates how SpecMAGIC coordinates individual reach-avoid tasks with dependency and count requirements. The planner updates agents’ subtasks as prerequisites are met, culminating in simultaneous and individual visits that satisfy the specifications.
Qualitative results
- The example combines individual reach-avoid tasks with dependencies among agents’ region visits and count constraints requiring simultaneous magenta visits and nonsimultaneous yellow visits.The trajectory visualization uses each timestep and the propositions true then; the planner visualization distinguishes selected subtask sequences from sampled alternatives.Source: E QUALITATIVE RESULTS · p. 19, Figure 7 · p. 19, Figure 8 · p. 20
- Initially, the planner assigns agent0 to reach yellow while avoiding green and magenta, agent1 to reach green while avoiding blue, magenta, and yellow, and agent2 to reach blue while avoiding magenta and yellow.After agent0 reaches yellow at t = 102, it can progress toward green, but green remains avoided until the prerequisite magenta1 is satisfied.Source: E QUALITATIVE RESULTS · p. 19
- After agent2 reaches blue at t = 198 and agent1 reaches magenta at t = 289, the planner updates subtasks; agents1 and 2 reach magenta simultaneously at t = 349, and the specifications are satisfied at t = 471.Agent0 reaches green at t = 358, while agent2 reaches yellow at t = 471.Source: E QUALITATIVE RESULTS · p. 20