OCTAL: Graph Representation Learning for LTL Model Checking

Model Checking is widely applied in verifying the correctness of complex and concurrent systems against a specification. Pure symbolic approaches while popular, suffer from the state space explosion problem due to cross product operations required that make them prohibitively expensive for large-scale systems and/or specifications. In this paper, we propose to use graph representation learning (GRL) for solving linear temporal logic (LTL) model checking, where the system and the specification are expressed by a B"uchi automaton and an LTL formula, respectively. A novel GRL-based framework model, is designed to learn the representation of the graph-structured system and specification, which reduces the model checking problem to binary classification. Empirical experiments on two model checking scenarios show that model achieves promising accuracy, with up to 11× overall speedup against canonical SOTA model checkers and 31× for satisfiability checking alone.