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.
2023
978-3-031-35354-3
978-3-031-35355-0
268
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11581/475205
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? ND
social impact