  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\"uchi 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.
