While Large Language Models (LLM) enable non-experts to specify open-world multi-robot tasks, the generated plans often lack kinematic feasibility and are not efficient, especially in long-horizon scenarios. Formal methods like Linear Temporal Logic (LTL) offer correctness and optimal guarantees, but are typically confined to static, offline settings and struggle with computational scalability. To bridge this gap, we propose a neuro-symbolic framework that grounds LLM reasoning into hierarchical LTL specifications and solves the corresponding Simultaneous Task Allocation and Planning (STAP) problem. Unlike static approaches, our system resolves stochastic environmental changes, such as moving users or updated instructions via a receding horizon planning (RHP) loop with real-time perception, which dynamically refines plans through a hierarchical state space. Extensive real-world experiments demonstrate that our approach significantly outperforms baseline methods in success rate and interaction fluency while minimizing planning latency.

翻译：尽管大型语言模型(LLM)使非专家能够指定开放世界的多机器人任务，但生成的规划通常缺乏运动学可行性且效率低下，尤其在长时域场景中。线性时序逻辑(LTL)等形式化方法能提供正确性与最优性保证，但通常局限于静态离线设置，且面临计算可扩展性挑战。为弥合这一差距，我们提出一种神经符号框架，将LLM推理嵌入层次化LTL规约，并求解对应的同步任务分配与规划(STAP)问题。与静态方法不同，我们的系统通过结合实时感知的滚动时域规划(RHP)循环处理随机环境变化（如移动用户或更新指令），借助层次化状态空间动态优化规划。大量真实世界实验表明，该方法在成功率和交互流畅度上显著优于基线方法，同时最大限度降低了规划延迟。