Checking LTL Satisfiability via End-to-end Learning

Linear temporal logic (LTL) satisfiability checking is a fundamental and hard (PSPACE-complete) problem. In this paper, we explore checking LTL satisfiability via end-to-end learning, so that we can take only polynomial time to check LTL satisfiability. Existing approaches have shown that it is possible to leverage end-to-end neural networks to predict the Boolean satisfiability problem with performance considerably higher than random guessing. Inspired by these approaches, we study two interesting questions: can end-to-end neural networks check LTL satisfiability, and can neural networks capture the semantics of LTL? To this end, we train different neural networks for keeping three logical properties of LTL, i.e., recursive property, permutation invariance, and sequentiality. We demonstrate that neural networks can indeed capture some effective biases for checking LTL satisfiability. Besides, designing a special neural network keeping the logical properties of LTL can provide a better inductive bias. We also show the competitive results of neural networks compared with state-of-the-art approaches, i.e., nuXmv and Aalta, on large scale datasets.