OCTAL: Graph Representation Learning for LTL Model Checking

TL;DR

This paper introduces OCTAL, a graph representation learning approach for LTL model checking that reduces computational complexity and achieves significant speedups over traditional methods.

Contribution

The paper presents a novel GRL-based framework for LTL model checking, addressing the state space explosion problem with improved efficiency.

Findings

Achieves up to 11x speedup over state-of-the-art model checkers.

Demonstrates promising accuracy in two model checking scenarios.

Provides a scalable alternative to symbolic model checking methods.

Abstract

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{\"u}chi 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\times$ overall speedup against canonical SOTA model checkers and $31\times$ for satisfiability checking alone.