Bridging LTLf Inference to GNN Inference for Learning LTLf Formulae

Learning linear temporal logic on finite traces (LTL f ) formulae aims to learn a target formula that characterizes the highlevel behavior of a system from observation traces in planning. Existing approaches to learning LTL f formulae, however, can hardly learn accurate LTL f formulae from noisy data. It is challenging to design an efficient search mechanism in the large search space in form of arbitrary LTL f formulae while alleviating the wrong search bias resulting from noisy data. In this paper, we tackle this problem by bridging LTL f inference to GNN inference. Our key theoretical contribution is showing that GNN inference can simulate LTL f inference to distinguish traces. Based on our theoretical result, we design a GNN-based approach, GLTLf, which combines GNN inference and parameter interpretation to seek the target formula in the large search space. Thanks to the non-deterministic learning process of GNNs, GLTLf is able to cope with noise. We evaluate GLTLf on various datasets with noise. Our experimental results confirm the effectiveness of GNN inference in learning LTL f formulae and show that GLTLf is superior to the state-of-the-art approaches.