Linear Temporal Logic (LTL) formulas have been used to describe complex tasks for multi-agent systems, with both spatial and temporal constraints. However, since the planning complexity grows exponentially with the number of agents and the length of the task formula, existing applications are mostly limited to small artificial cases. To address this issue, a new planning algorithm is proposed for task formulas specified as sc-LTL formulas. It avoids two common bottlenecks in the model-checking-based planning methods, i.e., (i) the direct translation of the complete task formula to the associated B\"uchi automaton; and (ii) the synchronized product between the B\"uchi automaton and the transition models of all agents. In particular, each conjuncted sub-formula is first converted to the associated R-posets as an abstraction of the temporal dependencies among the subtasks. Then, an efficient algorithm is proposed to compute the product of these R-posets, which retains their dependencies and resolves potential conflicts. Furthermore, the proposed approach is applied to dynamic scenes where new tasks are generated online. It is capable of deriving the first valid plan with a polynomial time and memory complexity w.r.t. the system size and the formula length. Our method can plan for task formulas with a length of more than 60 and a system with more than 35 agents, while most existing methods fail at the formula length of 20. The proposed method is validated on large fleets of service robots in both simulation and hardware experiments.

翻译：线性时序逻辑（LTL）公式已被用于描述多智能体系统中兼具空间与时间约束的复杂任务。然而，由于规划复杂度随智能体数量与任务公式长度呈指数增长，现有应用大多局限于小型人工案例。为解决此问题，针对以sc-LTL公式描述的任务规范提出了一种新型规划算法。该方法避免了基于模型检验的规划方法中两大常见瓶颈：（i）将完整任务公式直接翻译为对应的Büchi自动机；（ii）Büchi自动机与所有智能体转移模型的同步乘积。具体而言，首先将每个合取子公式转换为对应的R-偏序集，作为子任务间时序依赖关系的抽象。随后提出一种高效算法计算这些R-偏序集的乘积，该算法在保留其依赖关系的同时解决潜在冲突。此外，所提方法被应用于在线生成新任务的动态场景，能够在系统规模与公式长度上以多项式时间和内存复杂度推导出首个有效规划。我们的方法可为长度超过60的任务公式及超过35个智能体的系统进行规划，而现有方法在公式长度为20时即已失效。该方法的有效性已通过大规模服务机器人集群的仿真与硬件实验验证。