Guaranteed Satisfaction of a Signal Temporal Logic Formula on Tubes

Abstract

This paper considers the issue of how to deal with Signal Temporal Logic (STL) when taking into account uncertainties. The STL is a formalism with a large expressiveness to describe real-time properties on real-value signals. It is particularly used for system verification. This work focuses on extensions of STL that handle bounded uncertainties on predicates or on the signal itself, by using tubes to represent the sets of signals. In this way, it becomes possible to robustly check the satisfaction of specifications for a noisy system. However, some cases are undecidable due to uncertainty, and other ones are too complex to determine. Mainly, this paper provides a literature review and compares the few state-of-the-art STL monitors able to deal with tubes. In addition, it proposes to go further by introducing Boolean intervals to formalize undecidable cases, and by implementing a new STL formalism applied to sets in DynIbex, a guaranteed integration tool. Thus, STL specifications can be validated in a guaranteed way for a simulated system. As a result, we obtain the same reliable result as the state-of-the-art, but faster. A robotic application with a drone is proposed to illustrate the concept.