OCTAL: Graph Representation Learning for LTL Model Checking

TL;DR

OCTAL introduces a graph representation learning framework for LTL model checking, significantly improving speed while maintaining accuracy, thus addressing the state space explosion problem in traditional symbolic methods.

Contribution

The paper presents a novel GRL-based approach, OCTAL, that transforms LTL model checking into a binary classification task in latent space, offering a scalable alternative to symbolic methods.

Findings

Achieves comparable accuracy to state-of-the-art model checkers.

Provides up to 5x overall speedup in model checking.

Achieves over 63x speedup in satisfiability checking.

Abstract

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.