OCTAL: Graph Representation Learning for LTL Model Checking
This addresses efficiency issues in verifying complex systems for engineers and researchers, though it is an incremental improvement by applying existing GRL techniques to model checking.
The paper tackles the state space explosion problem in LTL model checking by using graph representation learning to reduce it to binary classification, achieving up to 11x overall speedup and 31x speedup for satisfiability checking against SOTA methods.
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{ü}chi 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\times$ overall speedup against canonical SOTA model checkers and $31\times$ for satisfiability checking alone.