A GNN Based Approach to LTL Model Checking

TL;DR

This paper introduces a GNN-based method for LTL model checking that transforms the problem into graph classification, significantly improving speed especially for large formulas and moderate models.

Contribution

It presents a novel GNN node embedding framework that encodes models and properties, reducing model checking to a graph classification task.

Findings

Up to 17 times faster than existing tools.

Effective for large LTL formulas and moderate models.

Reduces model checking to a graph classification problem.

Abstract

Model Checking is widely applied in verifying complicated and especially concurrent systems. Despite of its popularity, model checking suffers from the state space explosion problem that restricts it from being applied to certain systems, or specifications. Many works have been proposed in the past to address the state space explosion problem, and they have achieved some success, but the inherent complexity still remains an obstacle for purely symbolic approaches. In this paper, we propose a Graph Neural Network (GNN) based approach for model checking, where the model is expressed using a B{\"u}chi automaton and the property to be verified is expressed using Linear Temporal Logic (LTL). We express the model as a GNN, and propose a novel node embedding framework that encodes the LTL property and characteristics of the model. We reduce the LTL model checking problem to a graph classification problem, where there are two classes, 1 (if the model satisfies the specification) and 0 (if the model does not satisfy the specification). The experimental results show that our framework is up to 17 times faster than state-of-the-art tools. Our approach is particularly useful when dealing with very large LTL formulae and small to moderate sized models.