# OCTAL: Graph Representation Learning for LTL Model Checking

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 15 of its 48 references that are in the map.
- First posted on arXiv 19 Aug 2023.

## 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)

## Abstract (arXiv)

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.