TeLEx: Passive STL Learning Using Only Positive Examples
TeLEx: Passive STL Learning Using Only Positive Examples
复制标题
DOI：
10.1007/978-3-319-67531-2_13
复制
发表时间：
2017-09
期刊：
影响因子：
--
通讯作者：
Susmit Jha;Ashish Tiwari;S. Seshia;T. Sahai;Natarajan Shankar
中科院分区：
文献类型：
--
作者：
Susmit Jha;Ashish Tiwari;S. Seshia;T. Sahai;Natarajan Shankar
我们提出了一种新的被动学习方法，TELEX，它仅使用动态系统的观察信号轨迹来推导表征动态系统行为的信号时序逻辑公式。这种方法需要两个输入：一组观察到的轨迹和一个模板信号时序逻辑(STL)公式。模板中的未知参数可以包括时间算子的时间界限，也可以包括不等式预测中的阈值，TeLExe找到未知参数的值，使得合成的STL属性由所有提供的轨迹满足，并且它是紧的。这种严密的要求对于产生有趣的性质是必不可少的，当只提供积极的例子，并且没有主动查询动力系统以发现合法行为的边界的选项时。我们提出了一种新的满足STL性质的量化语义，使TeLEX能够在不进行多维优化的情况下学习紧密的STL性质。提出的新指标也是平滑的。这对基于梯度的数值优化引擎的使用至关重要，与最先进的无梯度优化相比，它的速度提高了30%-100%。该方法是在一个公开可用的工具中实现的。
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.TeLExfinds the value of the unknown parameters such that the synthesized STL property is satisfied by all the provided traces and it istight. This requirement oftightnessis 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 enablesTeLExto 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 30–100speed-up with respect to the state-of-art gradient-free optimization. The approach is implemented in a publicly available tool.