Interval Signal Temporal Logic from Natural Inclusion Functions

TL;DR

This paper introduces Interval Signal Temporal Logic ( ext{ISTL}), an extension of STL that handles uncertainty using interval arithmetic, enabling robust verification and control synthesis with minimal modifications to existing algorithms.

Contribution

The paper develops an interval extension of STL, called ISTL, allowing for uncertain signals and predicates, with straightforward integration into existing STL verification and synthesis tools.

Findings

Interval robustness can be computed using minimal inclusion functions.

ISTL enables verification and synthesis on uncertain signals with negligible computational overhead.

Demonstrated applications include offline monitoring and online control synthesis under uncertainty.

Abstract

We propose an interval extension of Signal Temporal Logic (STL) called Interval Signal Temporal Logic (\ISTL). Given an STL formula, we consider an interval inclusion function for each of its predicates. Then, we use minimal inclusion functions for the $\min$ and $\max$ functions to recursively build an interval robustness that is a natural inclusion function for the robustness of the original STL formula. The resulting interval semantics accommodate, for example, uncertain signals modeled as a signal of intervals and uncertain predicates modeled with appropriate inclusion functions. In many cases, verification or synthesis algorithms developed for STL apply to \ISTL with minimal theoretic and algorithmic changes, and existing code can be readily extended using interval arithmetic packages at negligible computational expense. To demonstrate \ISTL, we present an example of offline monitoring from an uncertain signal trace obtained from a hardware experiment and an example of robust online control synthesis enforcing an STL formula with uncertain predicates.