Research map / Multi-agent systems and games / Human-AI and goal-conditioned
Contract-based Design and Verification of Multi-Agent Systems with Quantitative Temporal Requirements
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Proposes good-enough decomposition contracts (GEDCs), a quantitative assume-guarantee contract framework for compositional LTL[F] specifications of multi-agent systems, with sound and complete decomposition and an automata-based compositional verification procedure.
Problem
Compositional design and verification of cooperative multi-agent systems whose quantitative temporal requirements (LTL[F]) combine local agent objectives with a shared safety constraint, where best-effort (good-enough) satisfaction is required and traditional boolean assume-guarantee contracts are i
Approach
Extends assume-guarantee contracts to quantitative specifications by pairing an allowed decompositions map (value decompositions of the overall LTL[F] value over local and shared sub-values, indexed by hopeful input sequences) with per-value assume-guarantee contracts, yielding a sound and complete decomposition rule for good-enough satisfaction.
Key results
- Compositional verification finishes on all six multi-agent benchmarks (3-6 agents) within the 30-minute timeout, while monolithic verification times out on delivery_vehicles and synchr_response.
- On tasks_scaled (6 agents, |Phi|=136), compositional verification takes 156 s versus 289 s for monolithic verification.
- Local revision (re-verifying a single modified agent) takes 0.2-24 s, faster than full compositional verification.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Use compositional verification instead of monolithic verification | GEDC verification · delivery_vehicles | runtime (seconds): TO vs 329 | Helped |
| Use compositional verification instead of monolithic verification | GEDC verification · tasks_collab | runtime (seconds): 34 vs 50 | Hurt |
| Use compositional verification instead of monolithic verification | GEDC verification · tasks_scaled | runtime (seconds): 289 vs 156 | Helped |
| Use compositional verification instead of monolithic verification | GEDC verification · robots_help_a3 | runtime (seconds): 1.3 vs 1.5 | Hurt |
| Use compositional verification instead of monolithic verification | GEDC verification · robots_help_a5 | runtime (seconds): 9.1 vs 15.7 | Hurt |
| Use compositional verification instead of monolithic verification | GEDC verification · synchr_response | runtime (seconds): TO vs 439 | Helped |
| Verify a local specification and implementation revision rather than the full system | Compositional verification · six MAS benchmarks | runtime (seconds): Rev. values: 24, 4, 13, 0.2, 3.1, 10; Comp. values: 329, 50, 156, 1.5, 15.7, 439 | Helped |
Surprising findings
- Monolithic verification is faster than compositional verification on the smallest benchmark (robots_help_a3: 1.3 s vs 1.5 s), since compositional overhead dominates for small specifications.
Limitations
- Worst-case complexity is double exponential in the size of the LTL[F] formula and polynomial/exponential in contract automata sizes.
- Failure of the contract check does not imply that the overall specification is violated, since the GEDC may be insufficient.
- Modifying a local specification to a weaker one can make an existing contract sub-optimal and require contract revision.
Experimental setup
Benchmarks: delivery_vehicles tasks_collab tasks_scaled robots_help_a3 robots_help_a5 synchr_response
Metrics: runtime (seconds)
Baselines: monolithic verification via product system
Builds on: LTL[F] assume-guarantee contracts good-enough synthesis generalized nondeterministic Büchi automata
Closest papers by meaning
- MAS-ProVe: Understanding the Process Verification of Multi-Agent Systems (ICML 2026 · similarity 0.86)
- LTLf Synthesis on First-Order Agent Programs in Nondeterministic Environments (AAAI 2025 · similarity 0.84)
- Benefits and Limitations of Communication in Multi-Agent Reasoning (ICLR 2026 · similarity 0.84)
- MAS-Orchestra: Understanding and Improving Multi-Agent Reasoning Through Holistic Orchestration and Controlled Benchmarks (ICML 2026 · similarity 0.83)
- On Alternating-Time Temporal Logic, Hyperproperties, and Strategy Sharing (AAAI 2024 · similarity 0.83)
- Natural Strategic Ability in Stochastic Multi-Agent Systems (AAAI 2024 · similarity 0.83)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.