Linear temporal logic (LTL) satisfiability checking is a fundamental and hard problem (PSPACE-complete). 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. Inspirited by their work, we study two interesting questions: can end-to-end neural networks check LTL satisfiability, and can neural networks learn the semantics of LTL. To this end, we train some neural networks with different architectures to explore the potential of neural networks on LTL satisfiability checking. We demonstrate that neural networks can indeed capture some effective biases for LTL satisfiability checking by training. Besides, designing a special architecture matching some logical properties of LTL, e.g., recursive property, permutation invariance, and sequentiality, can provide a better inductive bias. We also show the competitive results of neural networks compared with the state-of-the-art approaches, i.e., nuXmv and Aalta, on large scale datasets.

Weilin Luo

School of Computer Science and Engineering, Sun Yat-sen University

Hai Wan

School of Data and Computer Science, Sun Yat-sen University

China

Delong Zhang

SUN YAT-SEN UNIVERSITY

Jianfeng Du

Guangdong University of Foreign Studies

Hengdi Su

SUN YAT-SEN UNIVERSITY