Quantitative requirements play an important role in the context of multi-agent systems, where there is often a trade-off between the tasks of individual agents and the constraints that the agents must jointly adhere to. We study multi-agent systems whose requirements are formally specified in the quantitative temporal logic LTL[$\mathcal{F}$] as a combination of local task specifications for the individual agents and a shared safety constraint, The intricate dependencies between the individual agents entailed by their local and shared objectives make the design of multi-agent systems error-prone, and their verification time-consuming. In this paper we address this problem by proposing a novel notion of quantitative assume-guarantee contracts, that enables the compositional design and verification of multi-agent systems with quantitative temporal specifications. The crux of these contracts lies in their ability to capture the coordination between the individual agents to achieve an optimal value of the overall specification under any possible behavior of the external environment. We show that the proposed framework improves the scalability and modularity of formal verification of multi-agent systems against quantitative temporal specifications.

翻译：在智能体个体任务与系统整体约束之间常需权衡的多智能体系统背景下，定量需求具有重要作用。本文研究的多智能体系统需求通过定量时序逻辑LTL[$\mathcal{F}$]进行形式化规约，该规约融合了智能体个体的局部任务规约与系统共享的安全约束。由局部目标与共享目标引发的智能体间复杂依赖关系，使得多智能体系统的设计容易出错且验证耗时。本文通过提出创新的定量假设-保证契约概念来解决该问题，该契约支持具有定量时序规约的多智能体系统进行组合式设计与验证。此类契约的核心在于能够捕捉个体智能体间的协调机制，确保在外部环境任意可能行为下实现整体规约的最优值。研究表明，所提框架显著提升了多智能体系统针对定量时序规约的形式化验证的可扩展性与模块化程度。