Robust Online Monitoring of Signal Temporal Logic

Jyotirmoy Deshmukh, Alexandre Donzé, Shromona Ghosh, Xiaoqing Jin, Garvit Juniwal, and Sanjit A. Seshia. Robust Online Monitoring of Signal Temporal Logic. In Proceedings of the International Conference on Runtime Verification (RV), pp. 55–70, Lecture Notes in Computer Science 9333, Springer, September 2015.
Best Paper Award.

Download

[pdf] 

Abstract

Requirements of cyber-physical systems (CPS) can be rigorously specified using Signal Temporal Logic (STL). STL comes equipped with semantics that are able to quantify how robustly a given signal satisfies an STL property. In a setting where signal values over the entire time horizon of interest are available, efficient algorithms for offline computation of the robust satisfaction value have been proposed. Only a few methods exist for the online setting, i.e., where only a partial signal trace is available and rest of the signal becomes available in increments (such as in a real system or during numerical simulations). In this paper, we formalize the semantics for robust online monitoring of partial signals using the notion of robust satisfaction intervals (RoSIs). We propose an efficient algorithm to compute the RoSI and demonstrate its usage on two real-world case studies from the automotive domain and massively-online CPS education. As online algorithms permit early termination when the satisfaction or violation of a property is found, we show that savings in computationally expensive simulations far outweigh any overheads incurred by the online approach.

BibTeX

@inproceedings{deshmukh-rv15,
  author    = {Jyotirmoy Deshmukh and Alexandre Donz{\'{e}} and Shromona Ghosh and Xiaoqing Jin and Garvit Juniwal and Sanjit A. Seshia},
  title     = {Robust Online Monitoring of Signal Temporal Logic},
  booktitle = {Proceedings of the International Conference on Runtime Verification (RV)},
  Year = {2015},
  Month = {September},
  pages = {55--70},
  series    = {Lecture Notes in Computer Science},
  volume    = {9333},
  publisher = {Springer},
  wwwnote = {<b>Best Paper Award</b>.},
  abstract = {Requirements of cyber-physical systems (CPS) can be rigorously specified 
using Signal Temporal Logic (STL). STL comes equipped with semantics 
that are able to quantify how robustly a given signal satisfies an STL property. In 
a setting where signal values over the entire time horizon of interest are available, 
efficient algorithms for offline computation of the robust satisfaction value have 
been proposed. Only a few methods exist for the online setting, i.e., where only a 
partial signal trace is available and rest of the signal becomes available in increments 
(such as in a real system or during numerical simulations). In this paper, we 
formalize the semantics for robust online monitoring of partial signals using the 
notion of robust satisfaction intervals (RoSIs). We propose an efficient algorithm 
to compute the RoSI and demonstrate its usage on two real-world case studies 
from the automotive domain and massively-online CPS education. As online algorithms 
permit early termination when the satisfaction or violation of a property 
is found, we show that savings in computationally expensive simulations far outweigh 
any overheads incurred by the online approach.},
}