Bayesian Optimization for Polynomial Time Probabilistically Complete STL Trajectory Synthesis
This addresses efficiency issues in robotic and cyber-physical systems control by offering a faster, probabilistically complete alternative to MILP methods, though it is incremental as it trades completeness for speed.
The paper tackled the exponential complexity of STL trajectory synthesis by proposing a Bayesian optimization approach, achieving polynomial scaling in time-bound and linear scaling in predicates, with demonstrated scalability in a nontrivial example.
In recent years, Signal Temporal Logic (STL) has gained traction as a practical and expressive means of encoding control objectives for robotic and cyber-physical systems. The state-of-the-art in STL trajectory synthesis is to formulate the problem as a Mixed Integer Linear Program (MILP). The MILP approach is sound and complete for bounded specifications, but such strong correctness guarantees come at the price of exponential complexity in the number of predicates and the time bound of the specification. In this work, we propose an alternative synthesis paradigm that relies on Bayesian optimization rather than mixed integer programming. This relaxes the completeness guarantee to probabilistic completeness, but is significantly more efficient: our approach scales polynomially in the STL time-bound and linearly in the number of predicates. We prove that our approach is sound and probabilistically complete, and demonstrate its scalability with a nontrivial example.