We demonstrate the first Recurrent Neural Network architecture for learning
Signal Temporal Logic formulas, and present the first systematic comparison of
formula inference methods. Legacy systems embed much expert knowledge which is
not explicitly formalized. There is great interest in learning formal
specifications that characterize the ideal behavior of such systems -- that is,
formulas in temporal logic that are satisfied by the system's output signals.
Such specifications can be used to better understand the system's behavior and
improve design of its next iteration. Previous inference methods either assumed
certain formula templates, or did a heuristic enumeration of all possible
templates. This work proposes a neural network architecture that infers the
formula structure via gradient descent, eliminating the need for imposing any
specific templates. It combines learning of formula structure and parameters in
one optimization. Through systematic comparison, we demonstrate that this
method achieves similar or better mis-classification rates (MCR) than
enumerative and lattice methods. We also observe that different formulas can
achieve similar MCR, empirically demonstrating the under-determinism of the
problem of temporal logic inference.

本文介绍了一种新型的循环神经网络结构，可用于学习信号时间逻辑公式，并对公式推导方法进行了系统性比较。通过梯度下降训练神经网络，在不施加特定模板的情况下推导出公式结构和参数，可在实现类似分类误差率（MCR）的情况下发挥作用。研究人员还发现时间逻辑推断问题存在欠确定性。