A graph neural network is a deep learning architecture operating on graph-structured data. While they have achieved impressive results in many application domains, their applicability is limited when one needs to perform symbolic and semantic reasoning, for example, in model checking. We propose an approach based on the idea that graph neural networks can be programmed. We introduce μG, a simple language inspired by modal μ -calculus that can be compiled, via TensorFlow, in a graph neural network that can be efficiently run on parallel architectures. To demonstrate our method, we use our language to implement a Computation Tree Logic model checker. A benchmark from the Model Checking Contest is used to show that the performance of the resulting tool outperforms that of other model checkers.
Implementing a CTL Model Checker with μG, a Language for Programming Graph Neural Networks
Belenchia M.;Corradini F.;Quadrini M.;Loreti M.
2023-01-01
Abstract
A graph neural network is a deep learning architecture operating on graph-structured data. While they have achieved impressive results in many application domains, their applicability is limited when one needs to perform symbolic and semantic reasoning, for example, in model checking. We propose an approach based on the idea that graph neural networks can be programmed. We introduce μG, a simple language inspired by modal μ -calculus that can be compiled, via TensorFlow, in a graph neural network that can be efficiently run on parallel architectures. To demonstrate our method, we use our language to implement a Computation Tree Logic model checker. A benchmark from the Model Checking Contest is used to show that the performance of the resulting tool outperforms that of other model checkers.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
