An Operator-Based Approach to STL
For researchers in autonomous planning and control, this provides a more expressive and computationally tractable approach to STL-based verification and control.
The paper proposes a new operator-based framework for Signal Temporal Logic (STL) that handles complex multi-nested formulae and enables online control synthesis, demonstrated through theoretical conditions and simulations.
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.