December 11, 2025
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 Buchi automaton and an LTL formula, respectively. A novel GRL-based framework 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 it achieves promising accuracy, with up to 11 times overall speedup against canonical SOTA model checkers and 31 times for satisfiability checking alone.
About Prasita Mukherjee
Prasita Mukherjee is a PhD student working with Prof. Ben Delaware. Her research interests are in programming languages and neurosymbolic reasoning.