Past research into robotic planning with temporal logic specifications, notably Linear Temporal Logic (LTL), was largely based on singular formulas for individual or groups of robots. But with increasing task complexity, LTL formulas unavoidably grow lengthy, complicating interpretation and specification generation, and straining the computational capacities of the planners. By leveraging the intrinsic structure of tasks, we introduced a hierarchical structure to LTL specifications with requirements on syntax and semantics, and proved that they are more expressive than their flat counterparts. Second, we employ a search-based approach to synthesize plans for a multi-robot system, accomplishing simultaneous task allocation and planning. The search space is approximated by loosely interconnected sub-spaces, with each sub-space corresponding to one LTL specification. The search is predominantly confined to a single sub-space, transitioning to another sub-space under certain conditions, determined by the decomposition of automatons. Moreover, multiple heuristics are formulated to expedite the search significantly. A theoretical analysis concerning completeness and optimality is conducted under mild assumptions. When compared with existing methods on service tasks, our method outperforms in terms of execution times with comparable solution quality. Finally, scalability is evaluated by testing a group of 30 robots and achieving reasonable runtimes.

翻译：过去针对带有时序逻辑规约（尤其是线性时序逻辑LTL）的机器人规划研究，主要基于面向单个或群体机器人的单一公式。但随着任务复杂度的提升，LTL公式不可避免地变得冗长，导致解释和规约生成的复杂性增加，同时加重了规划器的计算负担。通过利用任务的内在结构，我们引入了一种具有语法和语义约束的分层LTL规约体系，并证明其表达能力优于扁平化规约。其次，采用基于搜索的方法为多机器人系统生成规划方案，实现了任务分配与规划的协同求解。搜索空间被近似分解为松散耦合的子空间，每个子空间对应一个LTL规约，搜索过程主要限定在单一子空间内，并在特定条件下（基于自动机分解判定）切换至其他子空间。此外，我们设计了多种启发式策略显著加速搜索过程。在温和假设下完成了关于完备性和最优性的理论分析。与现有服务型任务方法相比，本方法在保持相近解质量的前提下，执行时间更优。最后，通过30台机器人的群组测试验证了可扩展性，并获得了可接受的运行时间。