TeLEx: Passive STL Learning Using Only Positive Examples

Susmit Jha, Ashish Tiwari, Sanjit A. Seshia, Tuhin Sahai, and Natarajan Shankar. TeLEx: Passive STL Learning Using Only Positive Examples. In 17th International Conference on Runtime Verification (RV), pp. 208–224, 2017.

Download

[pdf] 

Abstract

We propose a novel passive learning approach, TeLEx, to infer signal temporal logic formulas that characterize the behavior of a dynamical system using only observed signal traces of the system. The approach requires two inputs: a set of observed traces and a template Signal Temporal Logic (STL) formula. The unknown parameters in the template can include time-bounds of the temporal operators, as well as the thresholds in the inequality predicates. TeLEx finds the value of the unknown parameters such that the synthesized STL property is satisfied by all the provided traces and it is tight. This requirement of tightness is essential to generating interesting properties when only positive examples are provided and there is no option to actively query the dynamical system to discover the boundaries of legal behavior. We propose a novel quantitative semantics for satisfaction of STL properties which enables TeLEx to learn tight STL properties without multidimensional optimization. The proposed new metric is also smooth. This is critical to enable use of gradient-based numerical optimization engines and it produces a 30X–100X speed-up with respect to the state-of-art gradient-free optimization. The approach is implemented in a publicly available tool.

BibTeX

@inproceedings{jha-rv17,
  author    = {Susmit Jha and
               Ashish Tiwari and
               Sanjit A. Seshia and
               Tuhin Sahai and
               Natarajan Shankar},
  title     = {TeLEx: Passive {STL} Learning Using Only Positive Examples},
  booktitle = {17th International Conference on Runtime Verification (RV)},
  pages     = {208--224},
  year      = {2017},
  abstract = {We propose a novel passive learning approach, TeLEx, to infer signal temporal logic formulas that characterize the behavior of a dynamical system using only observed signal traces of the system. The approach requires two inputs: a set of observed traces and a template Signal Temporal Logic (STL) formula. The unknown parameters in the template can include time-bounds of the temporal operators, as well as the thresholds in the inequality predicates. TeLEx finds the value of the unknown parameters such that the synthesized STL property is satisfied by all the provided traces and it is tight. This requirement of tightness is essential to generating interesting properties when only positive examples are provided and there is no option to actively query the dynamical system to discover the boundaries of legal behavior. We propose a novel quantitative semantics for satisfaction of STL properties which enables TeLEx to learn tight STL properties without multidimensional optimization. The proposed new metric is also smooth. This is critical to enable use of gradient-based numerical optimization engines and it produces a 30X–100X speed-up with respect to the state-of-art gradient-free optimization. The approach is implemented in a publicly available tool.},
}