pacSTL: PAC-Bounded Signal Temporal Logic from Data-Driven Reachability Analysis

TL;DR

pacSTL introduces a novel framework combining PAC-bounded set predictions with Signal Temporal Logic to enable safety monitoring of robotic systems under uncertainty, demonstrated through maritime navigation experiments.

Contribution

It presents the first PAC-bounded STL framework that integrates data-driven reachability analysis with temporal logic for safety assurance.

Findings

Effective in maritime navigation scenarios

Provides scalable and efficient safety monitoring

Demonstrates robustness intervals for specifications

Abstract

Real-world robotic systems must comply with safety requirements in the presence of uncertainty. To define and measure requirement adherence, Signal Temporal Logic (STL) offers a mathematically rigorous and expressive language. However, standard STL cannot account for uncertainty. We address this problem by presenting pacSTL, a framework that combines Probably Approximately Correct (PAC) bounded set predictions with an interval extension of STL through optimization problems on the atomic proposition level. pacSTL provides PAC-bounded robustness intervals on the specification level that can be utilized in monitoring. We demonstrate the effectiveness of this approach through maritime navigation and analyze the efficiency and scalability of pacSTL through simulation and real-world experimentation on model vessels.