STL Robustness Risk over Discrete-Time Stochastic Processes

TL;DR

This paper introduces a framework for assessing the risk of discrete-time stochastic processes satisfying signal temporal logic (STL) formulas, proposing an approximation method and data-driven estimation techniques for robustness risk.

Contribution

It defines the STL robustness risk for stochastic processes, proposes an upper-bound approximation, and develops a sampling-based data-driven estimation method.

Findings

The approximation provides an upper bound for the STL robustness risk.

Sampling-based methods effectively estimate the risk from data.

The framework accommodates various risk measures like conditional value-at-risk.

Abstract

We present a framework to interpret signal temporal logic (STL) formulas over discrete-time stochastic processes in terms of the induced risk. Each realization of a stochastic process either satisfies or violates an STL formula. In fact, we can assign a robustness value to each realization that indicates how robustly this realization satisfies an STL formula. We then define the risk of a stochastic process not satisfying an STL formula robustly, referred to as the STL robustness risk. In our definition, we permit general classes of risk measures such as, but not limited to, the conditional value-at-risk. While in general hard to compute, we propose an approximation of the STL robustness risk. This approximation has the desirable property of being an upper bound of the STL robustness risk when the chosen risk measure is monotone, a property satisfied by most risk measures. Motivated by the interest in data-driven approaches, we present a sampling-based method for estimating the approximate STL robustness risk from data for the value-at-risk. While we consider the value-at-risk, we highlight that such sampling-based methods are viable for other risk measures.