OCTAL: Graph Representation Learning for LTL Model Checking

07/24/2022
by   Prasita Mukherjee, et al.
0

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üchi 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.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset