OCTAL: Graph Representation Learning for LTL Model Checking
This addresses scalability issues in verifying complex systems for engineers and researchers, though it is an incremental improvement by applying existing GRL methods to a known bottleneck.
The paper tackles the state space explosion problem in LTL model checking by proposing OCTAL, a graph representation learning framework that reduces the problem to binary classification, achieving comparable accuracy to SOTA model checkers with up to 5x overall speedup and over 63x speedup for satisfiability checking.
Model Checking is widely applied in verifying the correctness of complex and concurrent systems against a specification. Pure symbolic approaches while popular, still suffer from the state space explosion problem that makes them impractical 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 OCTAL, is designed to learn the representation of the graph-structured system and specification, which reduces the model checking problem to binary classification in the latent space. The empirical experiments show that OCTAL achieves comparable accuracy against canonical SOTA model checkers on three different datasets, with up to $5\times$ overall speedup and above $63\times$ for satisfiability checking alone.