Simultaneous Task Allocation and Planning for Multi-Robots under Hierarchical Temporal Logic Specifications

Research in robotic planning with temporal logic specifications, such as linear temporal logic (LTL), has relied on single formulas. However, as task complexity increases, LTL formulas become lengthy, making them difficult to interpret and generate, and straining the computational capacities of planners. To address this, we introduce a hierarchical structure for a widely used specification type—LTL on finite traces (LTL<inline-formula><tex-math notation="LaTeX">$_{f}$</tex-math></inline-formula>). The resulting language, termed H-LTL<inline-formula><tex-math notation="LaTeX">$_{f}$</tex-math></inline-formula>, is defined with both its syntax and semantics. We further prove that H-LTL<inline-formula><tex-math notation="LaTeX">$_{f}$</tex-math></inline-formula> is more expressive than its standard “flat” counterparts. Moreover, we conducted a user study that compared the standard LTL<inline-formula><tex-math notation="LaTeX">$_{f}$</tex-math></inline-formula> with our hierarchical version and found that users could more easily comprehend complex tasks using the hierarchical structure. We develop a search-based approach to synthesize plans for multirobot systems, achieving simultaneous task allocation and planning. This method approximates the search space by loosely interconnected subspaces, each corresponding to an LTL<inline-formula><tex-math notation="LaTeX">$_{f}$</tex-math></inline-formula> specification. The search primarily focuses on a single subspace, transitioning to another under conditions determined by the decomposition of automata. We develop multiple heuristics to significantly expedite the search. Our theoretical analysis, conducted under mild assumptions, addresses completeness and optimality. Compared to existing methods used in various simulators for service tasks, our approach improves planning times while maintaining comparable solution quality.