Optimal Control Synthesis with Relaxed Global Temporal Logic Specifications for Homogeneous Multi-robot Teams
Disha Kamale, Cristian-Ioan Vasile
TL;DR
This work tackles control synthesis for a homogeneous team of robots under a global temporal logic specification when infeasibilities occur. It introduces a relaxed specification automaton built from a Time Window Temporal Logic ($TWTL$) formula and user-defined relaxation rules encoded as a Weighted Finite-State Edit System ($WFSE$), enabling minimal revisions with penalties. By combining automata-based representations with a carefully designed MILP encoding (MILP$_{\mathcal E}$) that avoids explicit product-automata construction, the approach jointly optimizes motion and specification relaxation, ensuring the progress towards satisfaction is explicit and optimizable. The method demonstrates feasibility and efficiency through case studies, illustrating improved expressivity over baselines and providing runtime insights for scalable deployment in multi-robot tasks.
Abstract
In this work, we address the problem of control synthesis for a homogeneous team of robots given a global temporal logic specification and formal user preferences for relaxation in case of infeasibility. The relaxation preferences are represented as a Weighted Finite-state Edit System and are used to compute a relaxed specification automaton that captures all allowable relaxations of the mission specification and their costs. For synthesis, we introduce a Mixed Integer Linear Programming (MILP) formulation that combines the motion of the team of robots with the relaxed specification automaton. Our approach combines automata-based and MILP-based methods and leverages the strengths of both approaches while avoiding their shortcomings. Specifically, the relaxed specification automaton explicitly accounts for the progress towards satisfaction, and the MILP-based optimization approach avoids the state-space explosion associated with explicit product-automata construction, thereby efficiently solving the problem. The case studies highlight the efficiency of the proposed approach.