pacSTL: PAC-Bounded Signal Temporal Logic from Data-Driven Reachability Analysis
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866918182066847744 |
|---|---|
| author | Dietrich, Elizabeth Krasowski, Hanna Gezer, Emir Cem Skjetne, Roger Sørensen, Asgeir Johan Arcak, Murat |
| author_facet | Dietrich, Elizabeth Krasowski, Hanna Gezer, Emir Cem Skjetne, Roger Sørensen, Asgeir Johan Arcak, Murat |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2511_00934 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | pacSTL: PAC-Bounded Signal Temporal Logic from Data-Driven Reachability Analysis Dietrich, Elizabeth Krasowski, Hanna Gezer, Emir Cem Skjetne, Roger Sørensen, Asgeir Johan Arcak, Murat Logic in Computer Science Robotics 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. |
| title | pacSTL: PAC-Bounded Signal Temporal Logic from Data-Driven Reachability Analysis |
| topic | Logic in Computer Science Robotics |
| url | https://arxiv.org/abs/2511.00934 |