Robustness Analysis for Value-Freezing Signal Temporal Logic

TL;DR

This paper introduces robustness measures for STL*, an extension of Signal Temporal Logic with value freezing, and presents an algorithm for robustness computation implemented in Parasim, demonstrated through case studies.

Contribution

It defines robustness measures for STL*, adapting from MTL, and provides an algorithm and tool for practical robustness analysis.

Findings

Robustness measures for STL* are successfully defined.

Algorithm for STL* robustness computation is developed and implemented.

Case studies demonstrate the effectiveness of the approach.

Abstract

In our previous work we have introduced the logic STL*, an extension of Signal Temporal Logic (STL) that allows value freezing. In this paper, we define robustness measures for STL* by adapting the robustness measures previously introduced for Metric Temporal Logic (MTL). Furthermore, we present an algorithm for STL* robustness computation, which is implemented in the tool Parasim. Application of STL* robustness analysis is demonstrated on case studies.