# OCTAL: Graph Representation Learning for LTL Model Checking

arXiv: https://arxiv.org/abs/2207.11649 · HTML: https://mlsanity.com/paper/2207.11649/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 15 of its 48 references that are in the map.
- First posted on arXiv 24 Jul 2022.

## Builds on (most cited first, 15 of 15)

- [Adam: A Method for Stochastic Optimization](https://mlsanity.com/paper/1412.6980/) (2014)
- [Semi-Supervised Classification with Graph Convolutional Networks](https://mlsanity.com/paper/1609.02907/) (2016)
- [Graph Attention Networks](https://mlsanity.com/paper/1710.10903/) (2017)
- [Inductive Representation Learning on Large Graphs](https://mlsanity.com/paper/1706.02216/) (2017)
- [Dropout as a Bayesian Approximation: Representing Model Uncertainty in Deep Learning](https://mlsanity.com/paper/1506.02142/) (2015)
- [How Powerful are Graph Neural Networks?](https://mlsanity.com/paper/1810.00826/) (2018)
- [Fast Graph Representation Learning with PyTorch Geometric](https://mlsanity.com/paper/1903.02428/) (2019)
- [GNNExplainer: Generating Explanations for Graph Neural Networks](https://mlsanity.com/paper/1903.03894/) (2019)
- [How Does Batch Normalization Help Optimization?](https://mlsanity.com/paper/1805.11604/) (2018)
- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [Generative Causal Explanations for Graph Neural Networks](https://mlsanity.com/paper/2104.06643/) (2021)
- [Graph Representations for Higher-Order Logic and Theorem Proving](https://mlsanity.com/paper/1905.10006/) (2019)
- [Teaching Temporal Logics to Neural Networks](https://mlsanity.com/paper/2003.04218/) (2020)
- [Two-stage Training of Graph Neural Networks for Graph Classification](https://mlsanity.com/paper/2011.05097/) (2020)
- [Graph Neural Reasoning for 2-Quantified Boolean Formula Solvers](https://mlsanity.com/paper/1904.12084/) (2019)

## Built on by (most cited first, 2 of 2)

- [Iterative Circuit Repair Against Formal Specifications](https://mlsanity.com/paper/2303.01158/) (2023)
- [A Neuro-Symbolic Framework for Sequence Classification with Relational and Temporal Knowledge](https://mlsanity.com/paper/2505.05106/) (2025)

## Abstract (arXiv)

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× overall speedup and above 63× for satisfiability checking alone.