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.
Thu 13 OctDisplayed time zone: Eastern Time (US & Canada) change
16:00 - 18:00 | Technical Session 32 - Formal Methods and Models IITool Demonstrations / Journal-first Papers / Research Papers at Banquet B Chair(s): Khouloud Gaaloul University of Michigan - Dearborn | ||
16:00 10mDemonstration | CBMC-SSM: Bounded Model Checking of C Programs with Symbolic Shadow Memory Tool Demonstrations Bernd Fischer Stellenbosch University, South Africa, Salvatore La Torre Università degli Studi di Salerno, Gennaro Parlato University of Molise, Peter Schrammel University of Sussex and Diffblue Ltd | ||
16:10 20mResearch paper | Tseitin or not Tseitin? The Impact of CNF Transformations on Feature-Model Analyses Research Papers Elias Kuiter Otto-von-Guericke-University Magdeburg, Sebastian Krieter University of Ulm, Chico Sundermann University of Ulm, Thomas Thüm University of Ulm, Gunter Saake University of Magdeburg, Germany | ||
16:30 20mPaper | A three-valued model abstraction framework for PCTL* stochastic model checkingVirtual Journal-first Papers Yang Liu Shanghai Maritime University/National University of Singapore, Yan Ma Nanjing University of Finance and Economics / National University of Singapore, Yongsheng Yang Shanghai Maritime University File Attached | ||
16:50 20mResearch paper | Finding and Understanding Incompleteness Bugs in SMT SolversVirtual Research Papers | ||
17:10 20mResearch paper | Checking LTL Satisfiability via End-to-end LearningVirtual Research Papers Weilin Luo School of Computer Science and Engineering, Sun Yat-sen University, Hai Wan School of Data and Computer Science, Sun Yat-sen University, Delong Zhang SUN YAT-SEN UNIVERSITY, Jianfeng Du Guangdong University of Foreign Studies, Hengdi Su SUN YAT-SEN UNIVERSITY | ||
17:30 20mResearch paper | QVIP: An ILP-based Formal Verification Approach for Quantized Neural NetworksVirtual Research Papers Yedi Zhang ShanghaiTech University, Zhe Zhao ShanghaiTech University, Guangke Chen ShanghaiTech University, Fu Song ShanghaiTech University, Min Zhang East China Normal University, Taolue Chen Birkbeck University of London, Jun Sun Singapore Management University |