End-to-End Learning of LTLf Formulae by Faithful LTLf Encoding

It is important to automatically discover the underlying treestructured formulae from large amounts of data. In this paper, we examine learning linear temporal logic on finite traces (LTL f ) formulae, which is a tree structure syntactically and characterizes temporal properties semantically. Its core challenge is to bridge the gap between the concise tree-structured syntax and the complex LTL f semantics. Besides, the learning quality is endangered by explosion of the search space and wrong search bias guided by imperfect data. We tackle these challenges by proposing an LTL f encoding method to parameterize a neural network so that the neural computation is able to simulate the inference of LTL f formulae. We first identify faithful LTL f encoding, a subclass of LTL f encoding, which has a one-to-one correspondence to LTL f formulae. Faithful encoding guarantees that the learned parameter assignment of the neural network can directly be interpreted to an LTL f formula. With such an encoding method, we then propose an end-to-end approach, TLTLf, to learn LTL f formulae through neural networks parameterized by our LTL f encoding method. Experimental results demonstrate that our approach achieves state-of-the-art performance with up to 7% improvement in accuracy, highlighting the benefits of introducing the faithful LTL f encoding.