<figure><img src="image_1.png" /></figure>

ifip

International Federation for Information Processing

This document is the original author manuscript of a paper submitted to an IFIP
conference proceedings or other IFIP publication by Springer Nature. As such, there
may be some differences in the official published version of the paper. Such
differences, if any, are usually due to reformatting during preparation for publication or
minor corrections made by the author(s) during final proofreading of the publication
manuscript.
# Implementing a CTL Model Checker with $\mu G$, a Language for Programming Graph Neural Networks

Matteo Belenchia(✉)D, Flavio CorradiniD, Michela QuadriniD, and Michele LoretiD

University of Camerino, Camerino, Italy
{matteo.belenchia,flavio.corradini,michela.quadrini,
michele.loreti}@unicam.it

**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 $\mu G$, a simple language inspired by modal $\mu$-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.

**Keywords:** Graph Neural Networks · Model checking · Computation Tree Logic

## 1 Introduction

Artificial Intelligence (AI) systems are being deployed in an increasing number of different tasks. In the last decade, there has been a renewed interest in Deep Learning (DL) models, such as neural networks, due to the increased computational capabilities of modern computers and the vast abundance of data in the Digital Age. Neural Networks [18] had stunning success in various tasks spanning computer vision, natural language processing, autonomous driving, software engineering, and more. Out of the many classes of neural network architectures, Graph Neural Networks (GNNs) emerged to deal specifically with graph-based data in the fields mentioned above. On the other hand, symbolic AI systems, which dominated the early years of AI, proved to be too brittle and unable to adapt to many of the tasks that nowadays machine learning systems can perform exceptionally well, and therefore gathered little interest from the industry and research community.
Our work stems from a simple question: *Can GNNs be used to improve model checking procedures?* Unfortunately, DL algorithms still have several limitations, including adversarial perturbations, unexplainability, catastrophic forgetting, and the inability to distinguish causation from correlation, to mention a few [29]. These issues make DL unsuitable for domains such as model-checking, where semantic and rule-based reasoning plays an important role. This is witnessed by the fact that neuro-symbolic computing has been proposed as an approach to combine the strengths of deep learning with those of symbolic AI [28, 30, 36].

In this paper, we propose combining neural and symbolic AI by defining $\mu G$, a formal language for the specification of graph neural networks. A $\mu G$ graph neural network consists of a composition of layers assembled according to the formal rules of the language, which may also be optimized during training in a supervised manner. The rules of $\mu G$ specify what transformations to perform on the input node-labeling of a graph and are loosely inspired from modal $\mu$-calculus [26]. Using our language allows the specification of graph neural networks that partly mitigate the problems typically associated with deep learning models outlined above.

For example, the outputs of a GNN can be explained according to the $\mu G$ terms that have been used to specify it. This approach does not make a $\mu G$ GNN completely explainable since it might still include opaque trainable components. Still, it is an improvement over the usual black-box approach of standard deep learning models.

More generally, our programming language allows selecting a reasonable trade-off between symbolic and neural computation. Once an appropriate level of detail has been chosen for a task [9], one could choose to use trainable functions (e.g., neural networks) to perform the sub-tasks where deep-learning usually excels, then use $\mu G$ to specify a GNN that performs the complete task using these functions as building blocks. The simpler the sub-tasks delegated to the trainable functions, the closer the final composite GNN resembles a purely symbolic algorithm. On the other hand, the more complex these sub-tasks, the more the final composite GNN resembles an ensemble of neural networks.

Furthermore, it is possible to avoid using trainable functions and completely specify a GNN without training it. A GNN of this kind can be used to implement any algorithm while also enjoying the computational benefits of deep learning models, namely the possibility of efficient computation on parallel architectures such as Graphic Processor Units (GPUs) and the portability of the code on any such architecture.

To show the advantages of the proposed approach, we apply $\mu G$ to develop a model checker for Computation Tree Logic (CTL [17]).

*Contributions.* Our main contributions are:

- We define the $\mu G$ language, its denotational semantics, and the typing of its expressions.

- We show how the $\mu G$ language can be implemented in Python using Tensor-Flow/Keras as the backend.
- We demonstrate how to use $\mu\mathcal{G}$ to program graph neural networks for CTL model checking.

- We show that the obtained tool outperforms two other existing tools, pyMod-elChecking and $\mu$CRL2, on a benchmark of the Model Checking Contest.

*Structure of the Paper.* In Sect. 2, we introduce the notation and preliminary information about graphs and graph neural networks. Then the $\mu\mathcal{G}$ language is described in Sect. 3 by its denotational semantics, while its Python implementation in TensorFlow is shown in Sect. 4. We evaluate the $\mu\mathcal{G}$ language on the task of CTL model checking in Sect. 5. Finally, we conclude with related work in Sect. 6 and future directions in Sect. 7.

## 2 Preliminaries and Notation

*Graphs and their Labelings.* A directed graph is a pair $G = (V, E)$ where $V$ is a collection of vertices (which we also refer to as “nodes”) and $E$ is a collection of ordered pairs of vertices, called edges. For any $u, v \in V$, whenever $(u, v) \in E$ we say that $u$ is a *predecessor* of $v$ and that $v$ is a *successor* of $u$. We also say that $(u, v)$ is an *incoming edge* for $v$ and an *outgoing edge* for $u$. Moreover, let $\overleftarrow{N}_G(v)$ denote the set of *predecessors* of $v$, formally $\overleftarrow{N}_G(v) = \{u \mid (u, v) \in E\}$, while $\overrightarrow{N}_G(u)$ denotes the set of *successors* of $u$, namely $\overrightarrow{N}_G(u) = \{v \mid (u, v) \in E\}$. Similarly, let $I_G(v)$ denote the set of *incoming edges* for $v$, formally $I_G(v) = \{(u, v) \mid u, v \in V\}$, and let $O_G(u)$ denote the set of *outgoing edges* for $u$, formally $O_G(u) = \{(u, v) \mid u, v \in V\}$.

Sometimes it is useful to associate nodes and edges with values. Given a graph $G = (V, E)$, we can consider its *node-labeling* and *edge-labeling*. The former is a function $\eta : V \to T_v$ associating each node $v \in V$ with a value in the set $T_v$. Similarly, an *edge-labeling* is a function $\xi : E \to T_e$ that maps an edge to its label in the set $T_e$. Let $V \subseteq V$ (resp. $E \subseteq E$), we let $\eta(V)$ (resp. $\xi(E)$) denote the *multi-set* of labels associated to the elements of $V$ (resp. $E$) by $\eta$ (resp. $\xi$). Likewise, we let $(\eta, \xi)(E)$ denote the *multi-set* of tuples $(\eta(u), \xi((u, v)), \eta(v))$ for each $(u, v) \in E$.

*Encoding of Graphs and Labels.* One way to represent graphs and their labeling functions on a computer is in the form of a matrix of node features $\mathbf{X}$, an adjacency matrix $\mathbf{A}$ and a matrix of edge features $\mathbf{E}$. The node features matrix $\mathbf{X}$ stores the features associated with each node in the graph. The $i$-th row of the matrix contains a value of type $\mathbf{x}_i \in T_v$ that represents the information associated with the $i$-th vertex of the graph in a given ordering. The adjacency matrix $\mathbf{A}$ encodes the architecture of the graph, with each non-zero element $a_{ij} \in \mathbb{R}$ denoting the presence of an edge from a node $i$ to a node $j$ with weight $a_{ij}$. The edge features matrix $\mathbf{E}$ stores the features associated with each edge, much like the node features matrix. The $i$-th row of $\mathbf{E}$ is a value of type $T_e$ that represents the information associated with the $i$-th edge in the row-major (or any other) ordering of the edges in $\mathbf{A}$.
*Graph Neural Networks.* A Graph Neural Network (GNN) is a deep learning model that operates on graph-structured data. Introduced by [35], it emerged to overcome the limitations of graph kernel methods [31]. GNNs are one of the most general classes of deep learning architecture: many other deep learning models can be seen as a particular case of graph neural networks [14].

Graph neural networks can be used for many tasks, which can be roughly categorized according to the subject of prediction: nodes, edges, or entire graphs. As with other machine learning models, there are two main kinds of tasks, namely classification and regression, where the goal is to predict the class or some numerical quantity associated with the nodes in the graph, edges, or entire graphs. What is different from other machine learning models is that the success of graph neural networks stems not from the assumption of independent and identically distributed data, but rather from the information that can be obtained from the dependencies of the data. GNNs may exploit concepts such as homophily, heterophily, the structural equivalence of nodes, or the small-world phenomenon [24].

The most general form of graph neural network, which subsumes most of the GNN variants that have been developed over the years [14], is the message passing neural network (MPNN) variant [8,21]. A typical MPNN comprises a fixed number of convolutional layers stacked in sequence, each updating the node features matrix. A convolution operation updates the features of all nodes in the graph at the same time, according to the following equation:

$$ \mathbf{x}'_i = u(\mathbf{x}_i, \oplus_{j \in N_G(i)} \varphi(\mathbf{x}_i, \mathbf{e}_{ij}, \mathbf{x}_j)) \quad (1) $$

where $N_G(i)$ is the set of neighbours of node $i$, $\oplus$ is a permutation-invariant function and $u, \varphi$ are learnable functions. The function $\varphi$ generates the message sent from node $j$ to node $i$, which in the simplest case might be the value of $\mathbf{x}_j$. The function $\oplus$ aggregates the multiset of messages obtained by $\varphi$ in a way that is independent of the order they are evaluated and is usually a non-learnable function such as the sum, product or mean, but, more generally, it can also be defined as a neural network. The function $u$ updates the embedding of node $i$ by considering both the current embedding $\mathbf{x}_i$ and the new embedding that was just computed.

Graph neural networks composed by layers described by Eq. 1 are permutation-equivariant functions that take as input a tuple $(\mathbf{X}, \mathbf{A}, \mathbf{E})$ and return a new node features matrix $\mathbf{X}'$. This characterization leaves out some types of graph neural networks, namely, the graph neural networks that use pooling layers (which therefore change the architecture of the graph by removing elements from $\mathbf{V}$ and $\mathbf{E}$) and the graph neural networks that learn edge features rather than node features (which therefore produce a new edge features matrix $\mathbf{E}'$ instead). At any rate, the standard graph neural network model we have just described is general enough to encompass these two special cases as well. A graph neural network that uses pooling layers can be represented by allowing the node-labeling function to label each node with an additional Boolean value that specifies whether the node has been deleted or not and by ruling that
an edge is valid if and only if both the source and destination nodes have not been deleted. A graph neural network that learns edge features can instead be modeled by reifying edges into nodes and by having the graph's node-labeling function label each node with an additional Boolean value that specifies whether the node represents an edge or a node of the original graph.

*Types.* We denote the set of all labeling functions with codomain $T$ as $H[T]$, and we say that this set specifies its *type*. As examples, labeling functions of type $H[\mathbb{B}]$ map vertices to Boolean values, while functions of type $H[\mathbb{N}^k]$ with $k \in \mathbb{N}$ map vertices to $k$-tuples of natural numbers. Given a graph $G$ together with its edge-labeling function $\xi$, we consider a graph neural network as a function $\phi_{G,\xi}: H[T_1] \to H[T_2]$ that maps a node-labeling function to another node-labeling function. We denote the set of graph neural networks as $\Phi_{G,\xi}[T_1, T_2]$ or, more succinctly, as $\Phi_{G,\xi}$. The subscript $G, \xi$ indicates that each graph neural network is parametrized by a graph and the edge-labeling function.

## 3 A Calculus of Graph Neural Networks

This section introduces the syntax of $\mu G$ as a programming language for graph neural networks. After defining the syntax (Definition 1), we show its denotational semantics (Definition 2).

**Definition 1.** (*Syntax*) Given a set $\mathcal{X} = \{X, Y, Z, \dots\}$ of variable symbols and a set $\mathcal{S}$ of function symbols, we define an algebra of Graph Neural Networks with the following abstract syntax:

$$ \mathcal{N} ::= \psi \mid \langle\phi_{\sigma} \mid \rangle_{\sigma} \mid \mathcal{N}_1; \mathcal{N}_2 \mid \mathcal{N}_1 || \mathcal{N}_2 \mid X \mid f(\mathcal{N}_1, \mathcal{N}_2, \dots, \mathcal{N}_k) \mid \\ \text{let } X = \mathcal{N}_1 \text{ in } \mathcal{N}_2 \mid \text{def } f(\tilde{X})\{\mathcal{N}_1\} \text{ in } \mathcal{N}_2 \mid \\ \text{if } \mathcal{N}_1 \text{ then } \mathcal{N}_2 \text{ else } \mathcal{N}_3 \mid \text{fix } X = \mathcal{N}_1 \text{ in } \mathcal{N}_2 $$

with $\phi, \sigma, \psi, f \in \mathcal{S}$ and $X \in \mathcal{X}$.

Given a graph $G$ and an edge-labeling $\xi$, the meaning of a $\mu G$ expression is a graph neural network, a function between node-labeling functions. One of the basic $\mu G$ terms is the *function application* $\psi$. This represents the application of a given function (referenced by $\psi$) to the input node-labeling function. Moreover, the *pre-image* operator $\langle\phi_{\sigma} \mid \rangle$ and the *post-image* operator $\rangle\phi_{\sigma}$ are used to compute the labeling of a node in terms of the labels of its predecessors and successors, respectively. Basic terms are composed by *sequential composition* $\mathcal{N}_1; \mathcal{N}_2$ and *parallel composition* $\mathcal{N}_1 || \mathcal{N}_2$. Local variables $X$ and functions $f(\tilde{X})$ can be defined using *let* and *def*. The *choice* operator *if* $\mathcal{N}_1$ *then* $\mathcal{N}_2$ *else* $\mathcal{N}_3$ allows to run different GNNs according to the result of a guard GNN. Finally, the *fixed point* operator $\text{fix } X = \mathcal{N}_1$ in $\mathcal{N}_2$ is used to program *recursive behavior*.

We say that a $\mu G$ term is *well-formed* whenever it can be typed with the rules of Table 1. These rules guarantee that any *well-formed* $\mu G$ term can be interpreted as a GNN. From now on, we will consider only *well-formed* terms.
**Definition 2.** (Denotational semantics) Given a graph $\mathcal{G}$ and an environment $\rho$ that comprises a variable evaluation function $\rho_v: \mathcal{X} \to \Phi_{\mathcal{G},\xi}$ and a function evaluation function $\rho_f: \mathcal{S} \to ((\Phi_{\mathcal{G},\xi} \times \dots \times \Phi_{\mathcal{G},\xi}) \to \Phi_{\mathcal{G},\xi})$ we define the semantic interpretation function $[\cdot]_{\rho}^{\mathcal{G},\xi}: \mathcal{N} \to \Phi_{\mathcal{G},\xi}$ on $\mu\mathcal{G}$ formulas $\mathcal{N}$ by induction in the following way:

$$[\psi]_{\rho}^{\mathcal{G},\xi}(\eta) = \lambda v.f_{\psi}(\eta(\mathcal{V}), \eta(v))$$

$$[\triangleq_{\sigma}^{\varphi}]_{\rho}^{\mathcal{G},\xi}(\eta) = \lambda v.f_{\sigma}(f_{\varphi}((\eta, \xi)(I_{\mathcal{G}}(v))), \eta(v))$$

$$[\triangleright_{\sigma}^{\varphi}]_{\rho}^{\mathcal{G},\xi}(\eta) = \lambda v.f_{\sigma}(f_{\varphi}((\eta, \xi)(O_{\mathcal{G}}(v))), \eta(v))$$

$$[\mathcal{N}_1; \mathcal{N}_2]_{\rho}^{\mathcal{G},\xi} = [\mathcal{N}_2]_{\rho}^{\mathcal{G},\xi} \circ [\mathcal{N}_1]_{\rho}^{\mathcal{G},\xi}$$

$$[\mathcal{N}_1 || \mathcal{N}_2]_{\rho}^{\mathcal{G},\xi}(\eta) = \lambda v. \langle ([\mathcal{N}_1]_{\rho}^{\mathcal{G},\xi}(\eta))(v), ([\mathcal{N}_2]_{\rho}^{\mathcal{G},\xi}(\eta))(v) \rangle$$

$$[X]_{\rho}^{\mathcal{G},\xi} = \rho(X)$$

$$[f(\mathcal{N}_1, \mathcal{N}_2, \dots, \mathcal{N}_k)]_{\rho}^{\mathcal{G},\xi} = \rho(f)([\mathcal{N}_1]_{\rho}^{\mathcal{G},\xi}, [\mathcal{N}_2]_{\rho}^{\mathcal{G},\xi}, \dots, [\mathcal{N}_k]_{\rho}^{\mathcal{G},\xi})$$

$$[\text{let } X = \mathcal{N}_1 \text{ in } \mathcal{N}_2]_{\rho}^{\mathcal{G},\xi} = [\mathcal{N}_2]_{\rho}[X \leftarrow [\mathcal{N}_1]_{\rho}^{\mathcal{G},\xi}]$$

$$[\text{def } f(\tilde{X})\{\mathcal{N}_1\} \text{ in } \mathcal{N}_2]_{\rho}^{\mathcal{G},\xi} = [\mathcal{N}_2]_{\rho}[f \leftarrow \lambda \tilde{X}', [\mathcal{N}_1]_{\rho}[\tilde{X} \leftarrow \tilde{X}']]$$

$$[\text{if } \mathcal{N}_1 \text{ then } \mathcal{N}_2 \text{ else } \mathcal{N}_3]_{\rho}^{\mathcal{G},\xi}(\eta) = \text{cond}([\mathcal{N}_1]_{\rho}^{\mathcal{G},\xi}, [\mathcal{N}_2]_{\rho}^{\mathcal{G},\xi}, [\mathcal{N}_3]_{\rho}^{\mathcal{G},\xi})(\eta)$$

$$[\text{fix } X = \mathcal{N}_1 \text{ in } \mathcal{N}_2]_{\rho}^{\mathcal{G},\xi}(\eta) = g([\mathcal{N}_1]_{\rho}^{\mathcal{G},\xi})(\eta)$$

For any $\psi, \varphi, \sigma, f \in \mathcal{S}$ and any $X \in \mathcal{X}$. The functions cond and g are defined as follows:

$$\text{cond}(t, f_1, f_2)(\eta) = \begin{cases} f_1(\eta) & \text{if } t(\eta) = \lambda v.\text{True} \\ f_2(\eta) & \text{otherwise} \end{cases}$$

$$g(\phi)(\eta) = \begin{cases} \phi(\eta) & \text{if } \phi(\eta) = [\mathcal{N}_2]_{\rho}^{\mathcal{G},\xi}(\eta) \\ g([\mathcal{N}_2]_{\rho}^{\mathcal{G},\xi})(\eta) & \text{otherwise} \end{cases}$$

In the following paragraphs, we clarify the denotational semantics of $\mu\mathcal{G}$ expressions.

**Function Application.** The function symbols $\psi_1, \psi_2, \dots \in \mathcal{S}$ are evaluated as the graph neural networks $[\psi_1]_{\rho}^{\mathcal{G},\xi}, [\psi_2]_{\rho}^{\mathcal{G},\xi}, \dots$ that map a node-labeling function $\eta$ to a new node-labeling function by applying a function on both local and global node information. The local information consists of applying $\eta$ to the input node, while the global information is the multiset of the labels of all the nodes in the graph. The graph neural network we obtain applies a possibly trainable function $f_{\psi}$ to these two pieces of information. Two particular cases arise if $f_{\psi}$ decides to ignore either of the two inputs. If $f_{\psi}$ ignores the global information, the GNN returns a node-labeling function $\eta_l$, a purely local transformation of the node labels. On the other hand, if $f_{\psi}$ ignores the local information, the GNN returns a
<table><caption>**Table 1.** Typing of $\mu\mathcal{G}$ expressions.</caption><tr><td>ψ</td><td><div style="text-align: right;">f<sub>ψ</sub>: T<sub>1</sub><sup>*</sup> × T<sub>1</sub> → T<sub>2</sub>, Γ ⊢ ψ : Φ<sub>g,ξ</sub>[T<sub>1</sub>, T<sub>2</sub>]</div></td></tr><tr><td>∠<sub>σ</sub><sup>ϕ</sup></td><td><div style="text-align: right;">f<sub>ϕ</sub>: T<sub>1</sub> × T<sub>e</sub> × T<sub>1</sub> → T<sub>2</sub>, f<sub>σ</sub>: T<sub>2</sub><sup>*</sup> × T<sub>1</sub> → T<sub>3</sub>, Γ ⊢ ∇<sub>σ</sub><sup>ϕ</sup> : Φ<sub>g,ξ</sub>[T<sub>1</sub>, T<sub>3</sub>]</div></td></tr><tr><td>▷<sub>σ</sub><sup>ϕ</sup></td><td><div style="text-align: right;">f<sub>ϕ</sub>: T<sub>1</sub> × T<sub>e</sub> × T<sub>1</sub> → T<sub>2</sub>, f<sub>σ</sub>: T<sub>2</sub><sup>*</sup> × T<sub>1</sub> → T<sub>3</sub>, Γ ⊢ ▷<sub>σ</sub><sup>ϕ</sup> : Φ<sub>g,ξ</sub>[T<sub>1</sub>, T<sub>3</sub>]</div></td></tr><tr><td>N<sub>1</sub>; N<sub>2</sub></td><td><div style="text-align: right;">Γ ⊢ N<sub>1</sub>: Φ<sub>g,ξ</sub>[T<sub>1</sub>, T<sub>2</sub>], N<sub>2</sub>: Φ<sub>g,ξ</sub>[T<sub>2</sub>, T<sub>3</sub>]<br>Γ ⊢ N<sub>1</sub>; N<sub>2</sub>: Φ<sub>g,ξ</sub>[T<sub>1</sub>, T<sub>3</sub>]</div></td></tr><tr><td>N<sub>1</sub>||N<sub>2</sub></td><td><div style="text-align: right;">Γ ⊢ N<sub>1</sub>: Φ<sub>g,ξ</sub>[T<sub>1</sub>, T<sub>2</sub>], N<sub>2</sub>: Φ<sub>g,ξ</sub>[T<sub>1</sub>, T<sub>2</sub>]<br>Γ ⊢ N<sub>1</sub>||N<sub>2</sub>: Φ<sub>g,ξ</sub>[T<sub>1</sub>, T<sub>2</sub> × T<sub>2</sub>]</div></td></tr><tr><td>X</td><td><div style="text-align: right;">Γ ⊢ X : Φ<sub>g,ξ</sub>[T<sub>1</sub>, T<sub>2</sub>]</div></td></tr><tr><td>f(N<sub>1</sub>,...,N<sub>k</sub>)</td><td><div style="text-align: right;">Γ ⊢ N<sub>1</sub>: Φ<sub>g,ξ</sub>[T<sub>1</sub>, T'<sub>1</sub>],...,N<sub>k</sub>: Φ<sub>g,ξ</sub>[T<sub>k</sub>, T'<sub>k</sub>]<br>Γ ⊢ f(N<sub>1</sub>,...,N<sub>k</sub>): Φ<sub>g,ξ</sub>[T, T']</div></td></tr><tr><td>let X = N<sub>1</sub> in N<sub>2</sub></td><td><div style="text-align: right;">Γ ⊢ N<sub>1</sub>: Φ<sub>g,ξ</sub>[T<sub>1</sub>, T<sub>2</sub>], Γ ∪ {X : Φ<sub>g,ξ</sub>[T<sub>1</sub>, T<sub>2</sub>]} ⊢ N<sub>2</sub>: Φ<sub>g,ξ</sub>[T, T']<br>Γ ⊢ let X = N<sub>1</sub> in N<sub>2</sub>: Φ<sub>g,ξ</sub>[T, T']</div></td></tr><tr><td>def f(&#773;X){N<sub>1</sub>} in N<sub>2</sub></td><td><div style="text-align: right;">Γ ∪ {X<sub>i</sub>: Φ<sub>g,ξ</sub>[T<sub>i</sub>, T'<sub>i</sub>] | i ∈ 1,...,k} ⊢ N<sub>1</sub>: Φ<sub>g,ξ</sub>[T<sub>0</sub>, T'<sub>0</sub>],<br>Γ ∪ {f : Φ<sub>g,ξ</sub>[T<sub>1</sub>, T'<sub>1</sub>] × ... × Φ<sub>g,ξ</sub>[T<sub>k</sub>, T'<sub>k</sub>] → Φ<sub>g,ξ</sub>[T<sub>0</sub>, T'<sub>0</sub>]} ⊢ N<sub>2</sub>: Φ<sub>g,ξ</sub>[T, T']<br>Γ ⊢ def f(&#773;X){N<sub>1</sub>} in N<sub>2</sub>: Φ<sub>g,ξ</sub>[T, T']</div></td></tr><tr><td>if N<sub>1</sub> then N<sub>2</sub> else N<sub>3</sub></td><td><div style="text-align: right;">Γ ⊢ N<sub>1</sub>: Φ<sub>g,ξ</sub>[T<sub>1</sub>, B], N<sub>2</sub>: Φ<sub>g,ξ</sub>[T<sub>1</sub>, T<sub>2</sub>], N<sub>3</sub>: Φ<sub>g,ξ</sub>[T<sub>1</sub>, T<sub>3</sub>]<br>Γ ⊢ if N<sub>1</sub> then N<sub>2</sub> else N<sub>3</sub>: Φ<sub>g,ξ</sub>[T<sub>1</sub>, T<sub>2</sub> ∪ T<sub>3</sub>]</div></td></tr><tr><td>fix X = N<sub>1</sub> in N<sub>2</sub></td><td><div style="text-align: right;">Γ ⊢ N<sub>1</sub>: Φ<sub>g,ξ</sub>[T<sub>1</sub>, T<sub>2</sub>], Γ ∪ {X : Φ<sub>g,ξ</sub>[T<sub>1</sub>, T<sub>2</sub>]} ⊢ N<sub>2</sub>: Φ<sub>g,ξ</sub>[T<sub>1</sub>, T<sub>2</sub>]<br>Γ ⊢ fix X = N<sub>1</sub> in N<sub>2</sub>: Φ<sub>g,ξ</sub>[T<sub>1</sub>, T<sub>2</sub>]</div></td></tr></table>

node-labeling function $\eta_g$ that assigns to each node a label that summarizes the entire graph, emulating what in the GNN literature is known as a *global pooling* operator [23].

**Pre-image and Post-Image.** The pre-image symbol $\langle\cdot\rangle$ and the post-image symbol $\triangleright$, together with function symbols $\varphi \in S$ and $\sigma \in S$ are evaluated as the graph neural networks $[\langle\varphi\rangle_{\rho}^{G,\xi}$ and $[\triangleright_{\sigma}^{\varphi}]_{\rho}^{G,\xi}$ for any $\sigma, \varphi \in S$. In the case of the pre-image, for any symbol $\varphi \in S$ the corresponding function $f_{\varphi}$ generates a message from a tuple $(\eta(u), \xi((u, v)), \eta(v))$, and this is repeated for each $(u, v) \in I_G(v)$. Then for any symbol $\sigma \in S$ the corresponding function $f_{\sigma}$ generates a new label for a node $v$ from the multiset of messages obtained from $f_{\varphi}$ and the current label $\eta(v)$. The functions $f_{\varphi}$ and $f_{\sigma}$ may be trainable. The case of the post-image is analogous, with the difference that $f_{\varphi}$ is applied to tuples $(\eta(v), \xi((v, u)), \eta(u))$ for each $(v, u) \in O_G(v)$ instead.

**Sequential Composition.** An expression of the form $N_1:N_2$ for $\mu\mathcal{G}$ formulas $N_1,N_2$ is evaluated as the graph neural network $[N_2;N_1]_{\rho}^{G,\xi}$ that maps a node-labeling function $\eta$ to a new node-labeling function obtained from the function composition of $[N_2]_{\rho}^{G,\xi}$ and $[N_1]_{\rho}^{G,\xi}$.
**Parallel Composition.** An expression of the form $N_1||N_2$ for $\mu G$ formulas $N_1, N_2$ is evaluated as the graph neural network $[[N_2||N_1]]_\rho^{G,\xi}$ that maps a node-labelling function $\eta$ to a new node-labelling function that maps a node $v$ to the tuple $\langle [[N_1]]_\rho^{G,\xi}(\eta)(v), [[N_2]]_\rho^{G,\xi}(\eta)(v) \rangle$. Moreover, combining this operator with the basic function symbols $\psi_1, \psi_2, \dots \in S$ allows the execution of k-ary operations on the node-labelling functions: a k-ary function application $f_{op_k}(N_1, \dots, N_k)$ is expressible as the $\mu G$ expression $((\dots (N_1||N_2)||\dots)||N_k); op_k$.

**Choice.** The choice operator if $N_1$ then $N_2$ else $N_3$ for $\mu G$ formulas $N_1, N_2, N_3$ is evaluated as the graph neural network $[[N_2]]_\rho^{G,\xi}$ if $\eta' = [[N_1]]_\rho^{G,\xi}(\eta)$ is a node-labelling function such that $\forall v \in G, \eta'(v) = \text{True}$. Otherwise it is evaluated as the graph neural network $[[N_3]]_\rho^{G,\xi}$.

**Fixed Points.** The fixed point operator is evaluated as the graph neural network that is obtained by applying $[[N_1]]_\rho^{G,\xi}$ to the least fixed point of the functional $\mathcal{F}[32]$ associated to $g$. Formally, it is $\bigcup\{\mathcal{F}^n | n \ge 0\}([N_1]_\rho^{G,\xi})$ where

$$ \mathcal{F}^0 = \lambda\phi.\lambda\eta.\perp \\ \mathcal{F}^{n+1} = \mathcal{F}(\mathcal{F}^n) $$

# 4 From $\mu G$ to TensorFlow

One of the main advantages of using GNNs is related to the widespread availability of Python libraries that allow their development. We chose to implement $\mu G$ using Spektral [22], based on the well-known TensorFlow/Keras framework, because of its easy-to-use APIs to represent graphs, implement new GNN layers and batch graphs together. Another advantage of libraries such as TensorFlow is that once we have a graph neural network model, it can be executed on any architecture without changes. This means a $\mu G$ program can be run without modification on a CPU, GPU, or TPU. Furthermore, in TensorFlow, it is straightforward to distribute input data across multiple devices. Therefore, it is possible to split the input data to be run on multiple GPUs in parallel.

In the following paragraphs, we describe how each of the $\mu G$ expressions is translated into TensorFlow/Keras layers using Spektral APIs. These layers can then be composed together into a single graph neural network model. Intermediate outputs of the model can be re-used: if the same $\mu G$ sub-formula occurs more than once as part of the same $\mu G$ expression, its results are computed only once and re-used wherever they are needed.

**Function Application.** The function application operator is implemented by a layer that applies the function $f_\psi$ to the input node features matrix $X$. Therefore, even though we defined $f_\psi$ in two arguments, we really only provide the first: a local operation on every node-labeling value can be performed efficiently and
in parallel because TensorFlow broadcasts arithmetic operations. For example, if we are interested in adding 1 to every label, a function $f_1(\mathbf{X}) = \mathbf{X} + 1$ suffices because 1 is broadcast to every row of $\mathbf{X}$.

**Pre-image and Post-image.** For the pre-image and post-image operators, we developed the corresponding layers that compute a multiset of messages for each node using $f_\phi$ and then aggregate them using $f_\sigma$. The sparse adjacency matrix $\mathbf{A}$ is stored in memory as a $(|\mathbf{E}|, 2)$ matrix, with each row representing an edge that originates in the node of the first column and ends in the node of the second column. Therefore the inputs for the function $f_\phi$ are three sequences: the labels of the nodes in the first column of $\mathbf{A}$, the edge labels $\mathbf{E}$ and the labels of the nodes in the second column of $\mathbf{A}$. The function will be applied row by row on these three input sequences in parallel using broadcasting. The messages are then passed to $f_\sigma$ together with the nodes to which each message should be "sent": for the pre-image operator, this is the first column of $\mathbf{A}$, while for the post-image operator, it is the second column instead. Additionally, we make $f_\sigma$ accept the total number of nodes in the graph because TensorFlow offers very efficient functions to aggregate values which require the number of aggregations to be performed.

**Sequential Composition.** The sequential composition of graph neural networks is straightforward: the model is built by composing in sequence the left-hand side graph neural network model with the right-hand side one, with the output of the former becoming the input of the latter.

**Parallel Composition.** The parallel composition of graph neural networks is a model that is built by concatenating the left-hand side graph neural network model with the right-hand side one. This type of operation is common enough that it is already available in TensorFlow with the **Concatenate** layer. Therefore it simply suffices to send the outputs of the two models as inputs to the **Concatenate** layer.

**Choice Operator.** The choice operator is a model that is built using TensorFlow's `cond` function: the arguments of this function are the output of the graph neural network that computes the Boolean test and the two graph neural networks that are to be run according to the condition.

**Fixed Point Computation.** For the fixed point operator `fix X = N_1 in N_2`, we first evaluate the argument $N_2$. If no variable $X$ occurs in $N_2$, then `fix X = N_1 in N_2$ simplifies to $N_2$. In all other cases, $N_2$ will contain zero or more sub-expressions independent of $X$ and one or more sub-expressions that depend on $X$. We build the parse tree for $N_2$ and construct models $M_1, M_2, \dots, M_k$ for any sub-tree that is independent of $X$. The values produced by these models become inputs of the fixed point layer. The fixed point layer is characterized by a model $M$ in exactly $k+1$ inputs, the first $k$ of them to be bound to the outputs of models $M_1, \dots, M_k$ and the last argument to be bound, initially, to
the value produced by $N_1$. The layer performs a looping operation, each time running $M$ with the same $k$ arguments but with the previously obtained output as the value of the $k + 1$-th argument. When the output of $M$ is the same as the value of $k + 1$-th input argument, it is returned as output. For floating point labels, it is possible to specify an absolute tolerance value such that two labels are considered equal if they differ by less than the tolerance value.

# 5 $\mu G$ in Action: A CTL Model Checker

This section shows how $\mu G$ can be used to program a model checker for CTL formulas. To the best of our knowledge, neither GPU-accelerated CTL model-checking algorithms nor machine learning models for this task have been proposed. Our approach enables using GNNs for CTL model checking that can be executed on parallel architectures such as GPUs. Notably, we need not use trainable functions for this task. In Sect. 5.1, we recall the basics of Computation Tree Logic model checking, then in Sect. 5.2, we show how to translate each CTL formula to a $\mu G$ term that labels each node of a graph with a Boolean value indicating if the formula is satisfied or not in the state represented by that node. Finally, in Sect. 5.3, we evaluate the $\mu G$-programmed CTL model checker against two other model checking tools on Petri net models from the Model Checking Contest.

## 5.1 Basics of Computation Tree Logic

Computation Tree Logic (CTL) is a branching-time logic interpreted over Kripke structures. A Kripke structure is a directed graph whose nodes correspond to the states of a system and whose edges correspond to state transitions. More formally, let $AP$ be a set of atomic propositions, then a Kripke structure is a tuple $\mathcal{K} = (S, I, R, L)$ where $S$ is a finite set of states, $I \subseteq S$ is a set of initial states, $R \subseteq S \times S$ is a transition relation between states, and $L: S \to 2^{AP}$ is a labeling function that associates each state to a set of atomic propositions. Let $p \in AP$, a CTL formula can be generated using the following grammar:

$$ \phi ::= p | \neg\phi | \phi_1 \land \phi_2 | EX\phi | EG\phi | E\phi_1 U \phi_2 $$

We recall that a path $\pi = s_1 s_2 \dots$ is an infinite sequence of states such that $\forall i, (s_i, s_{i+1}) \in R$. We let $Path(s)$ denote the set of paths originating from $s$, while for any path $\pi$, $\pi[i]$ denotes the $i$-th state in $\pi$.

Given a Kripke structure $\mathcal{K} = (S, I, R, L)$, a set of atomic propositions $AP$ and a well-formed CTL formula $\phi$, we define the semantics of a CTL formula as a set of states $[[\phi]]_\mathcal{K}$ in the following way:
<caption>**Table 2.** Recursive definition of the translation function $\mathcal{M} : \phi \to \mathcal{N}$.</caption>

$$
\begin{align*}
\mathcal{M}(p) &= \psi_p \qquad \mathcal{M}(\neg\phi) = \mathcal{M}(\phi); \psi_{\neg} \\
\mathcal{M}(\phi_1 \land \phi_2) &= (\mathcal{M}(\phi_1) || \mathcal{M}(\phi_2)); \psi_{\land} \qquad \mathcal{M}(EX\phi) = \mathcal{M}(\phi); \triangleright_{\sigma_{\vee}}^{\phi_{pr3}} \\
\mathcal{M}(EG\phi) &= \mathbf{fix} \ X = \psi_{true} \ \mathbf{in} \ ((\mathcal{M}(\phi) || (X; \triangleright_{\sigma_{\vee}}^{\phi_{pr3}})); \psi_{\land}) \\
\mathcal{M}(E\phi_1 U \phi_2) &= \mathbf{fix} \ X = \psi_{false} \ \mathbf{in} \ (\mathcal{M}(\phi_2) || ((\mathcal{M}(\phi_1) || (X; \triangleright_{\sigma_{\vee}}^{\phi_{pr3}})); \psi_{\land}); \psi_{\vee})
\end{align*}
$$

$$
\begin{align*}
[\![p]]_{\mathcal{K}} &= \{s \mid p \in L(s)\} \\
[\neg\phi]_{\mathcal{K}} &= S \setminus [[\phi]]_{\mathcal{K}} \\
[\phi_1 \land \phi_2]_{\mathcal{K}} &= [[\phi_1]]_{\mathcal{K}} \cap [[\phi_2]]_{\mathcal{K}} \\
[EX\phi]_{\mathcal{K}} &= \{s \mid \exists s' \text{ s.t. } (s, s') \in R \land s' \in [[\phi]]_{\mathcal{K}}\} \\
[EG\phi]_{\mathcal{K}} &= \{s \mid \exists \pi \text{ s.t. } \pi[0] = s \land \forall i, \pi[i] \in [[\phi]]_{\mathcal{K}}\} \\
[E \phi_1 U \phi_2]_{\mathcal{K}} &= \{s \mid \exists \pi \text{ s.t. } \pi[0] = s \land \exists k \forall i < k \pi[i] \in [[\phi_1]]_{\mathcal{K}} \land \pi[k] \in [[\phi_2]]_{\mathcal{K}}\}
\end{align*}
$$

## 5.2 Computation Tree Logic in $\mu\mathcal{G}$

Let $\phi$ be a CTL formula. Then we can define a graph neural network $\text{SAT}_{\varphi}: H[2^{AP}] \to H[\mathbb{B}]$ where the input node-labeling function is the Kripke structure's labeling function, and the output node-labeling function assigns a **True** label to every node that satisfies $\varphi$ and a **False** label to every node that doesn't. The translation function $\mathcal{M}: \phi \to \mathcal{N}$ that maps CTL expressions to $\mu\mathcal{G}$ terms is shown in Table 2. The function symbols used in the table are to be intended as follows: $\psi_p$ denotes a function

$$f_p(\cdot, l) = \begin{cases} \text{True} & \text{if } p \in l \\ \text{False} & \text{otherwise} \end{cases}$$

that maps a node's label $l$ to **True** if and only if $p \in L(s)$, and we have one such function for any $p \in AP \cup \{\text{True, False}\}$. Function symbols $\psi_\wedge, \psi_\vee, \psi_\neg$ denote the usual Boolean connectives (which, like $f_p$, ignore their first argument), $\sigma_{\max}$ denotes the max aggregation function for multisets and finally $\varphi_{pr3}$ denotes the projection function that returns its third argument.

**Theorem 1.** Let $\mathcal{K} = (S, I, R, L)$ be a Kripke structure, let $\mathcal{G} = (S, R)$ be the corresponding graph, and let $\mathcal{M}$ be the function recursively translating CTL formulas to $\mu\mathcal{G}$ as in Table 2. Then for every state $s \in S$ we have that:

$$s \in [[\phi]]_{\mathcal{K}} \implies [[\mathcal{M}(\phi)]]_{\rho}^{G, \xi}(L)(s) = \text{True}$$

$$s \notin [[\phi]]_{\mathcal{K}} \implies [[\mathcal{M}(\phi)]]_{\rho}^{G, \xi}(L)(s) = \text{False}$$

*Proof.* The proof is standard and follows the same structure used to prove the correctness of the translation from CTL to $\mu$-calculus [13, 20].
<table><caption>**Table 3.** Petri net models used for the experiments, for which we reported here the number of nodes and edges in the reachability graph (RG).</caption><thead><tr><td>ID</td><td>Petri Net</td><td>#nodes in RG</td><td>#edges in RG</td></tr></thead><tbody><tr><td>1</td><td>RobotManipulation-PT-00001</td><td>110</td><td>274</td></tr><tr><td>2</td><td>TokenRing-PT-005</td><td>166</td><td>365</td></tr><tr><td>3</td><td>Philosophers-PT-000005</td><td>243</td><td>945</td></tr><tr><td>4</td><td>RobotManipulation-PT-00002</td><td>1430</td><td>5 500</td></tr><tr><td>5</td><td>Dekker-PT-010</td><td>6144</td><td>171 530</td></tr><tr><td>6</td><td>BART-PT-002</td><td>17 424</td><td>53 328</td></tr><tr><td>7</td><td>ClientsAndServers-PT-N0001P0</td><td>27 576</td><td>113 316</td></tr><tr><td>8</td><td>Philosophers-PT-000010</td><td>59 049</td><td>459 270</td></tr><tr><td>9</td><td>Referendum-PT-0010</td><td>59 050</td><td>393 661</td></tr><tr><td>10</td><td>SatelliteMemory-PT-X00100Y0003</td><td>76 358</td><td>209 484</td></tr><tr><td>11</td><td>RobotManipulation-PT-00005</td><td>184 756</td><td>1 137 708</td></tr><tr><td>12</td><td>Dekker-PT-015</td><td>278 528</td><td>16 834 575</td></tr><tr><td>13</td><td>HouseConstruction-PT-00005</td><td>1 187 984</td><td>7 191 110</td></tr></tbody></table>

## 5.3 Evaluation

We compare the performance of the $\mu G$ CTL model checker introduced in the previous section with two other existing tools: pyModelChecking<fnref n="1" />, which implements a CTL model checker in Python, and the $\mu$CRL2 toolset [15], which is a well-known and broadly used model checker.

We consider the Petri net models from the Model Checking Contest 2022 (MCC2022) [1]. Among the available models, we selected those for which it was possible to generate the reachability graph (RG). These models are summarised in Table 3. For each model, there are 16 CTL formulas for which we have to compute the set of satisfying states.

Our experiment measured the total time it took to verify these 16 formulas for each Petri net model. It was performed on a Windows 11 machine with an Intel Core i7-10875H CPU, NVIDIA GeForce RTX 2070 Max-Q GPU with 6GiB of VRAM, and 16GiB of RAM.

We consider two execution setups for $\mu G$. In the first setup, which we refer to as the “split” setup, we verify each of the 16 CTL formulas one by one by first generating the corresponding graph neural network model and then running it on the Kripke structure obtained from the Petri net. In the second setup, which we call the “full” setup, we model-check all 16 formulas at once, in parallel, by concatenating the expression corresponding to each formula with the parallel composition operator of $\mu G$. This second approach can obtain considerable speedups compared to the first but is at risk of running out of memory. For both the setups, we also report the time spent to generate the TensorFlow

<footnote n="1">¹ https://github.com/albertocasagrande/pyModelChecking.</footnote>
computation graph, an operation commonly referred to as “tracing”. A computation graph defines the data flow of the computations to perform, with nodes representing operations and arrows representing the flow of data. This tracing phase has to be performed only once for each $\mu G$ model, after which the model can be used without retracing the graph. The pyModelChecking Python library is used to verify each formula one by one on the Kripke structure, as in the case of the $\mu G$ split setup. Finally, in the case of $\mu$CRL2, we use the Petri net’s labeled transition system and convert the CTL formulas into the equivalent $\mu$-calculus formulas. Then for each formula, we record the time needed to generate the corresponding parametrized boolean equation system (PBES) and the time it takes for $\mu$CRL2 to solve it. The PBES is generated using the `lts2pbes` command with the `-p` argument, which may lead to smaller PBESs. Then the PBES is solved using the `pbessolve` command with the `-threads=8` argument to allow the best multi-threaded performance possible on our machine.

The experimental results are shown in Table 4. For each instantiated Petri net model, we report the computation graph generation and execution times. For $\mu G$, we report the time for the split model, where the total time needed to model check all the formulas is shown, and for the full model. The last two columns in the table show the $\mu$CRL2 time for generating and solving the PBESs.

<table><caption>**Table 4.** Execution times for $\mu G$ models, pyModelChecking and $\mu$CRL2.</caption><thead><tr><th>Petri Net</th><th>Tracing (split)</th><th>Running (split)</th><th>Tracing (full)</th><th>Running (full)</th><th>pyMC</th><th>μCRL2 PBES gen.</th><th>μCRL2 PBES solv.</th></tr></thead><tbody><tr><td>1</td><td>7.541 s</td><td>0.406 s</td><td>6.494 s</td><td>0.17 s</td><td>0.048 s</td><td>0.476 s</td><td>0.118 s</td></tr><tr><td>2</td><td>13.534 s</td><td>0.552 s</td><td>7.704 s</td><td>0.189 s</td><td>0.203 s</td><td>10.822 s</td><td>0.128 s</td></tr><tr><td>3</td><td>9.379 s</td><td>0.426 s</td><td>8.441 s</td><td>0.174 s</td><td>0.125 s</td><td>2.345 s</td><td>0.13 s</td></tr><tr><td>4</td><td>8.655 s</td><td>0.609 s</td><td>7.974 s</td><td>0.264 s</td><td>0.863 s</td><td>5.739 s</td><td>0.142 s</td></tr><tr><td>5</td><td>9.926 s</td><td>0.684 s</td><td>8.621 s</td><td>0.176 s</td><td>6.001 s</td><td>132.027 s</td><td>0.164 s</td></tr><tr><td>6</td><td>25.265 s</td><td>4.987 s</td><td>12.21 s</td><td>0.958 s</td><td>24.399 s</td><td>481.579 s</td><td>0.161 s</td></tr><tr><td>7</td><td>9.593 s</td><td>1.603 s</td><td>8.677 s</td><td>0.727 s</td><td>17.53 s</td><td>105.978 s</td><td>0.173 s</td></tr><tr><td>8</td><td>8.928 s</td><td>2.008 s</td><td>7.401 s</td><td>0.619 s</td><td>52.184 s</td><td>1031.431 s</td><td>0.219 s</td></tr><tr><td>9</td><td>10.404 s</td><td>1.79 s</td><td>9.491 s</td><td>0.476 s</td><td>51.117 s</td><td>610.559 s</td><td>0.237 s</td></tr><tr><td>10</td><td>8.515 s</td><td>3.942 s</td><td>7.826 s</td><td>1.359 s</td><td>28.542 s</td><td>214.721 s</td><td>0.209 s</td></tr><tr><td>11</td><td>8.727 s</td><td>4.940 s</td><td>8.094 s</td><td>1.492 s</td><td>136.821 s</td><td>1232.92 s</td><td>0.366</td></tr><tr><td>12</td><td>10.493 s</td><td>16.593 s</td><td>8.911 s</td><td>OOM</td><td>497.917 s</td><td>12551.7 s</td><td>4.227 s</td></tr><tr><td>13</td><td>9.008 s</td><td>61.964 s</td><td>8.445 s</td><td>25.003 s</td><td>936.875 s</td><td>7160.645 s</td><td>1.884 s</td></tr></tbody></table>

Except for the smallest graphs, both the full and split $\mu G$ models are faster than pyModelChecking, even when taking into account the one-time cost of building the computation graph. The split $\mu G$ model is also slightly slower than the full model, as expected, but it is able to successfully solve the Dekker-PT-015 task without running out of memory, which the full model could not. In comparison to $\mu$CRL2, we notice that the solution of PBESs with 8 threads is very fast, much faster than running the $\mu G$ model. On the other hand, the generation of PBESs is a very time-consuming task that has to be performed
for each combination of graphs and formulas: verifying the same formula on two different graphs requires two different PBESs. Therefore, if we consider the total time it takes for $\mu$CRL2 to generate and solve the PBESs, we conclude again that, except for the smallest instances, $\mu G$ requires far less time to verify all the formulas. This is clearly exemplified by the already mentioned Dekker-PT-015 dataset, for which $\mu G$ is able to verify all the formulas in under 30 s, while $\mu$CRL2 needs almost three hours and a half. Despite these positive results, a model checker based on $\mu G$ has also a number of drawbacks. Not only can the $\mu G$ model only be used if the full graph fits into the GPU memory, but it is further limited by the complexity of the CTL formula to verify: very “wide” formulas that require keeping in memory many different node-labeling functions of the graph at the same time are more likely to exhaust memory, even if the graph itself may not be very large. In contrast, other model-checking tools do not have memory limitations associated with the complexity of the formulas to verify.

# 6 Related Work

We surveyed the literature by looking at previous work on the topic of model checking tools that either use machine learning or are executed on GPUs.

The contributions of machine learning to model checking were, until recently, limited to helping classical model checkers to find invalidating runs more quickly or reducing the rate of spurious counterexamples [2]. More recently, at least two attempts have been made to implement a model checker using only machine learning models. Both attempts have in common that the requirement of providing an exact answer to all queries is relaxed, therefore changing the task to approximate model checking.

Neural Model Checking is the first such attempt [33]. The authors use neural networks to learn a graph-specific classifier trained on the graphs' execution traces. They focus on continuous and hybrid systems and only consider time-bounded reachability properties, but their method can be applied both online and offline and claims a prediction accuracy greater than 99%.

The second attempt [41] consists in predicting the output of a Linear Temporal Logic (LTL [34]) model checker given the encodings of an LTL formula and a Kripke structure. While the framework can boast very high prediction accuracy and claims to avoid the state explosion problem altogether, it cannot generalize to different sizes of input data. The authors note that the network is unable to generalize what it learned to Kripke structures of different sizes and formulae of different lengths.

A lot of work has been devoted in the past decade to developing GPU-accelerated model checkers. A commented list of these tools, none of which considers CTL model checking, is reported below. All these approaches rely on hand-crafting low-level code that can be executed on a GPU. In contrast, $\mu G$ is a high-level language that completely abstracts from the underlying architecture: the same $\mu G$ program can be run on a CPU, GPU, or TPU. The use of
TensorFlow, or any other high-level machine learning library, guarantees that executions will be optimized for the available hardware.

For LTL model checking, DiVinE-CUDA [4–6] is an explicit-state model checker that runs accepting cycle detection algorithms on possibly multiple GPUs. Cycles are detected using either the Maximal Accepting Predecessor algorithm (MAP) or the One-Way-Catch-Them-Young (OWCTY) algorithm, while a parallel algorithm on the CPU explicitly generates the state space. On-the-fly reachability checking was tackled by GPURC [40] using breadth-first search with dynamic load balancing. Another approach for GPU-accelerated LTL model checking is the work in [7], where the authors re-implement Holzmann’s parallel BFS algorithm used by the multi-core SPIN model checker. Later, the same authors developed Grapple [19], an explicit-state swarm verification model checker.

Liveness properties have been first tackled in [37], which use Rabin automata and Breadth-First Search with piggybacking. The most recent work in the context of LTL safety property model checking on GPUs used the Forward-Backward algorithm [16].

Another GPU-accelerated model checker is GPUexplore [39], which can be used to check for deadlocks and verify safety properties on-the-fly [38]. GPU-explore works on networks of labeled transition systems, which are assumed to represent parallel processes, and the formulas are represented as LTSs too.

For the case of quantitative analysis, the first LTLC model checker for GPUs uses a mixed DFS-BFS algorithm for solving multiple feasibility checking problems in parallel [27]. A GPU-accelerated model checker for Probabilistic Computation Tree Logic (PCTL [25]) based on PRISM was developed and described by [10–12], which use a parallel implementation of the Jacobi method.

# 7 Conclusion

We have presented $\mu G$, a formal language that allows programming GNNs. The latter can be seen as a higher-order function $\phi_{G,\xi}: H[T_1] \rightarrow H[T_2]$. An application of the language for the task of CTL model checking is shown and evaluated against other model-checking tools.

In the future, we plan to apply $\mu G$ to other tasks: in the context of model checking, we would like to apply our approach for the model checking of probabilistic and stochastic logics such as PCTL and CSL [3].

The applications of $\mu G$ are not limited to model checking. Indeed, we will investigate the use of $\mu G$ on more standard GNN tasks. In particular, we will use our approach to solve typical data analysis problems. The starting point is the analysis of the CORA citation network dataset, which has already been performed with $\mu G$ but is omitted here due to space constraints.

Finally, we will also study the integration of standard learning techniques that have been used with GNNs in our language. Note that, in this work, we have not considered functions that can be optimized. Nevertheless, one could consider parametric functions that can be learned in a supervised setting.
## References

1. Amparore, E., et al.: Presentation of the 9th edition of the model checking contest. In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.) TACAS 2019. LNCS, vol. 11429, pp. 50–68. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17502-3_4

2. Amrani, M., Lúcio, L., Bibal, A.: ML + FV = ♡? A Survey on the Application of Machine Learning to Formal Verification. arXiv:1806.03600 (2018). http://arxiv.org/abs/1806.03600

3. Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Verifying continuous time Markov chains. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 269–276. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-61474-5_75

4. Barnat, J., Brim, L., Ceška, M., Lamr, T.: CUDA accelerated LTL model checking. In: 2009 15th International Conference on Parallel and Distributed Systems, pp. 34–41 (2009). https://doi.org/10.1109/ICPADS.2009.50. ISSN 1521-9097

5. Barnat, J., Bauch, P., Brim, L., Češka, M.: Designing fast LTL model checking algorithms for many-core GPUs. J. Parallel Distrib. Comput. **72**(9), 1083–1097 (2012). https://doi.org/10.1016/j.jpdc.2011.10.015. https://www.sciencedirect.com/science/article/pii/S0743731511002140

6. Barnat, J., Brim, L., Češka, M.: DiVinE-CUDA - a tool for GPU accelerated LTL model checking. Electron. Proc. Theor. Comput. Sci. **14**, 107–111 (2009). https://doi.org/10.4204/EPTCS.14.8. http://arxiv.org/abs/0912.2555. http://arxiv.org/abs/0912.2555. arXiv:0912.2555

7. Bartocci, E., DeFrancisco, R., Smolka, S.A.: Towards a GPGPU-parallel SPIN model checker. In: Proceedings of the 2014 International SPIN Symposium on Model Checking of Software, San Jose CA USA, pp. 87–96. ACM (2014). https://doi.org/10.1145/2632362.2632379. https://dl.acm.org/doi/10.1145/2632362.2632379

8. Battaglia, P.W., et al.: Relational inductive biases, deep learning, and graph networks (2018). https://arxiv.org/abs/1806.01261v3. arXiv:1806.01261

9. Belenchia, M., Thórisson, K.R., Eberding, L.M., Sheikhlar, A.: Elements of task theory. In: Goertzel, B., Iklé, M., Potapov, A. (eds.) AGI 2021. LNCS (LNAI), vol. 13154, pp. 19–29. Springer, Cham (2022). https://doi.org/10.1007/978-3-030-93758-4_3

10. Bosnacki, D., Edelkamp, S., Sulewski, D., Wijs, A.: Parallel probabilistic model checking on general purpose graphics processors. Int. J. Softw. Tools Technol. Transfer **13**, 21–35 (2011). https://doi.org/10.1007/s10009-010-0176-4

11. Bošnački, D., Edelkamp, S., Sulewski, D.: Efficient probabilistic model checking on general purpose graphics processors. In: Păsăreanu, C.S. (ed.) SPIN 2009. LNCS, vol. 5578, pp. 32–49. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02652-2_7

12. Bošnački, D., Edelkamp, S., Sulewski, D., Wijs, A.: GPU-PRISM: an extension of PRISM for general purpose graphics processing units. In: 2010 Ninth International Workshop on Parallel and Distributed Methods in Verification, and Second International Workshop on High Performance Computational Systems Biology, pp. 17–19 (2010). https://doi.org/10.1109/PDMC-HiBi.2010.11

13. Bradfield, J., Walukiewicz, I.: The mu-calculus and model checking. In: Clarke, E., Henzinger, T., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 871–919. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-10575-8_26
14. Bronstein, M.M., Bruna, J., Cohen, T., Veličković, P.: Geometric Deep Learning: Grids, Groups, Graphs, Geodesics, and Gauges (2021). https://doi.org/10.48550/arXiv.2104.13478. http://arxiv.org/abs/2104.13478. http://arxiv.org/abs/2104.13478. arXiv:2104.13478

15. Bunte, O., et al.: The mCRL2 toolset for analysing concurrent systems. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11428, pp. 21–39. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17465-1_2

16. Chu, C., Luo, G., Zhang, M.: An optimized model checking parallel algorithm based on CUDA. In: 2019 IEEE 18th International Conference on Cognitive Informatics Cognitive Computing (ICCI*CC), pp. 446–452 (2019). https://doi.org/10.1109/ICCICC46617.2019.9146097

17. Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982). https://doi.org/10.1007/BFb0025774

18. Dastres, R., Soori, M.: Artificial neural network systems. Int. J. Imaging Robot. (IJIR) 21(2), 13–25 (2021). https://hal.archives-ouvertes.fr/hal-03349542

19. DeFrancisco, R., Cho, S., Ferdman, M., Smolka, S.A.: Swarm model checking on the GPU. Int. J. Softw. Tools Technol. Transf. 22(5), 583–599 (2020). https://doi.org/10.1007/s10009-020-00576-x

20. Emerson, E.A.: Model checking and the mu-calculus. Descriptive Complex. Finite Models 31, 185–214 (1996)

21. Gilmer, J., Schoenholz, S.S., Riley, P.F., Vinyals, O., Dahl, G.E.: Neural Message Passing for Quantum Chemistry. arXiv:1704.01212 (2017). http://arxiv.org/abs/1704.01212. arXiv:1704.01212

22. Grattarola, D., Alippi, C.: Graph Neural Networks in TensorFlow and Keras with Spektral. arXiv:2006.12138 (2020). http://arxiv.org/abs/2006.12138. arXiv: 2006.12138

23. Grattarola, D., Zambon, D., Bianchi, F.M., Alippi, C.: Understanding pooling in graph neural networks. IEEE Trans. Neural Netw. Learn. Syst. 1–11 (2022). https://doi.org/10.1109/TNNLS.2022.3190922

24. Hamilton, W.L.: Graph representation learning. Synth. Lect. Artif. Intell. Mach. Learn. 14(3), 1–159 (2020)

25. Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Form. Aspects Comput. 6(5), 512–535 (1994). https://doi.org/10.1007/BF01211866

26. Kozen, D.: Results on the propositional μ-calculus. In: Nielsen, M., Schmidt, E.M. (eds.) ICALP 1982. LNCS, vol. 140, pp. 348–359. Springer, Heidelberg (1982). https://doi.org/10.1007/BFb0012782

27. Kwon, Y.M., Kim, E.: A design of GPU-based quantitative model checking. In: Henglein, F., Shoham, S., Vizel, Y. (eds.) VMCAI 2021. LNCS, vol. 12597, pp. 441–463. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-67067-2_20

28. Lamb, L.C., D'avila Garcez, A., Gori, M., Prates, M.O.R., Avelar, P.H.C., Vardi, M.Y.: Graph neural networks meet neural-symbolic computing: a survey and perspective. In: Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence (2020)

29. Marcus, G.: Deep learning: a critical appraisal (2018). https://arxiv.org/abs/1801.00631. arXiv:1801.00631

30. Marcus, G.: The Next Decade in AI: Four Steps Towards Robust Artificial Intelligence (2020). https://arxiv.org/abs/2002.06177v3. arXiv:2002.06177
31. Morris, C., Fey, M., Kriege, N.: The power of the Weisfeiler-Leman algorithm for machine learning with graphs. In: Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, pp. 4543–4550. International Joint Conferences on Artificial Intelligence Organization, Montreal, Canada (2021). https://doi.org/10.24963/ijcai.2021/618. https://www.ijcai.org/proceedings/2021/618

32. Nielson, H.R., Nielson, F.: Denotational semantics. In: Nielson, H.R., Nielson, F. (eds.) Semantics with Applications: An Appetizer, pp. 91–126. Springer, Heidelberg (2007). https://doi.org/10.1007/978-1-84628-692-6_5

33. Phan, D., Grosu, R., Paoletti, N., Smolka, S.A., Stoller, S.D.: How to Learn a Model Checker. arXiv:1712.01935 (2017). http://arxiv.org/abs/1712.01935. arXiv: 1712.01935

34. Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science (SFCS 1977), pp. 46–57 (1977). https://doi.org/10.1109/SFCS.1977.32. ISSN 0272-5428

35. Scarselli, F., Gori, M., Tsoi, A.C., Hagenbuchner, M., Monfardini, G.: The graph neural network model. IEEE Trans. Neural Netw. 20(1), 61–80 (2009). https://doi.org/10.1109/TNN.2008.2005605

36. Susskind, Z., Arden, B., John, L.K., Stockton, P., John, E.B.: Neuro-symbolic AI: an emerging class of AI workloads and their characterization. CoRR abs/2109.06133 (2021). https://arxiv.org/abs/2109.06133

37. Wijs, A.: BFS-based model checking of linear-time properties with an application on GPUs. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 472–493. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41540-6_26

38. Wijs, A., Bošnački, D.: Many-core on-the-fly model checking of safety properties using GPUs. Int. J. Softw. Tools Technol. Transfer 18(2), 169–185 (2015). https://doi.org/10.1007/s10009-015-0379-9

39. Wijs, A., Bošnački, D.: GPUexplore: many-core on-the-fly state space exploration using GPUs. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 233–247. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54862-8_16

40. Wu, Z., Liu, Y., Sun, J., Shi, J., Qin, S.: GPU accelerated on-the-fly reachability checking. In: 2015 20th International Conference on Engineering of Complex Computer Systems (ICECCS), pp. 100–109 (2015). https://doi.org/10.1109/ICECCS.2015.21

41. Zhu, W., Wu, H., Deng, M.: LTL model checking based on binary classification of machine learning. IEEE Access (2019). https://doi.org/10.1109/ACCESS.2019.2942762