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. In order to maximize the potential of LTL specifications, we capitalized on the intrinsic structure of tasks and introduced a hierarchical structure to LTL specifications, and designed an algorithm to ascertain whether they are satisfied given an input sequence. 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规约的分层架构，并设计了算法来判定给定输入序列是否满足这些规约。其次，我们采用基于搜索的方法为多机器人系统综合规划，实现任务分配与规划的同步进行。搜索空间由松散耦合的子空间近似构成，每个子空间对应一个LTL规约。搜索过程主要限定在单一子空间内，仅在特定条件下根据自动机分解结果切换至另一子空间。此外，我们设计多种启发式策略显著加速搜索过程。在温和假设下，我们进行了完备性和最优性的理论分析。与服务任务上的现有方法相比，我们的方法在执行时间上更优，且解质量相当。最后，通过测试30个机器人群组并获得合理运行时间，验证了方法的可扩展性。