Search papers, labs, and topics across Lattice.
This paper introduces a novel operator-based approach to Signal Temporal Logic (STL) that acts on reachability value functions, providing a new theoretical framework for handling complex, multi-nested formulae. The key innovation lies in developing operator-based nesting rules directly, rather than focusing on STL-based reachability or control barrier functions. Theoretical analysis provides necessary and sufficient conditions for STL formula satisfaction, and simulations demonstrate the method's expressiveness with complex fragments.
Forget designing reachability functions for STL; this work offers operator-based nesting rules that directly tackle complex, multi-nested formulas and enable online control synthesis.
Signal Temporal Logic (STL), has recently seen extensive development, owing to its rich expressivenes for autonomous planning and control. Nevertheless, existing verification and control synthesis methods are limited with respect to the complexity and degree of nesting of the formulae. In this work, we propose a novel approach to STL based on an operator acting on reachability value functions. This constitutes a new theoretical framework for handling complex multi-nested formulae while at the same time providing tools for on-line control synthesis. In contrast to focusing on the design of STL-based reachability (or control barrier) functions, we develop operator-based nesting rules directly. Our method's expressiveness is demonstrated both theoretically, where necessary and sufficient conditions for STL formula satisfaction are extracted, as well as in simulations with complex fragments.
