A Modal Logic for Explaining some Graph Neural Networks
In this paper, we propose a modal logic in which counting modalities appear
in linear inequalities. We show that each formula can be transformed into an
equivalent graph neural network (GNN). We also show that each GNN can be
transformed into a formula. We show that the satisfiability problem is
decidable. We also discuss some variants that are in PSPACE.
Pierre Nunn, François Schwarzentruber
# A Modal Logic for Explaining some Graph Neural Networks

###### Abstract

In this paper, we propose a modal logic in which counting modalities appear in linear inequalities. We show that each formula can be transformed into an equivalent graph neural network (GNN). We also show that each GNN can be transformed into a formula. We show that the satisfiability problem is decidable. We also discuss some variants that are in PSPACE.

## 1 Introduction

Graph neural networks are used to learn a class of graphs or pointed graphs (a graph with a designated vertex). GNNs are used in many applications: social networks [16], chemistry, knowledge graphs etc. (see [25] for an overview of the applications of GNNs). The Saint-Graal for explaning GNNs would be to provide an algorithm for the following problem:

**Synthesis of an explanation**

* input: a GNN \(A\)
* output: a logical formula \(\varphi\) such that \([[A]]=[[\varphi]]\)

where \([[A]]\) is the class of pointed graphs recognized by the GNN \(A\), and \([[\varphi]]\) is the class of pointed graphs in which \(\varphi\) holds. In other words, the goal is to compute a formula \(\varphi\) (in modal logic, or in graded modal logic for example) that completely explains the class of graphs recognized by \(A\).

For instance, in a social network, a person is recommended by a GNN \(A\) iff that person has at least one friend that is musician (the formula \(\varphi\) being for instance expressed in modal logic by \(\Diamondmusician\), where \(\Diamond\) is the existential modal operator). The synthesis of an explanation in some logic - let say first-order logic, modal logic, or graded modal logic - is highly challenging. In this paper, we tackle a less challenging problem but that goes in the same direction. We provide an algorithmic solution for tackling the following problems:

**P1: Verification of an explanation**

* input: a GNN \(A\), a logical formula \(\varphi\)
* output: yes, if \([[A]]\subseteq[[\varphi]]\)
#### 1.0.1 P3: Verification of an explanation P4: Finding a counterexample

* input: a GNN \(A\), a logical formula \(\varphi\)
* output: yes, if \([[\varphi]]\cap[[A]]\neq\emptyset\)

Here are kind of question instances that problems P1-4 are able to solve:

* P1: is a recommended person a person that has at least one musician friend?
* P2: does any recommended person have a musician friend?
* P3: is any person that a musician friend recommended?
* P4: is it possible to recommend a person that has at least one musician friend?

Our solution is a general methodology to solve the problems P1-4 which consists in representing everything (\(\varphi\) but also the GNN \(A\)) in logic. Interestingly, there is a neat correspondence between graded modal logic and GNNs ([3], [8]). Graded modal logic [6] is a modal logic offering the ability via the construction \(\diamondsuit^{\geq k}\varphi\) to say that a vertex has more that \(k\) successors satisfying a formula \(\varphi\) We know that a GNN that is expressible in first-order logic (FO) is also captured by a formula in graded modal logic [3]. However the use of graded modal logic is problematic because we do not know how to represent _any_ GNN into it (in particular those who are not expressible in FO).

That is why we define a logic called \(K^{\#}\) which is more expressive enough to capture a reasonable class of GNNs while being able to express any formula in modal logic or graded modal logic. We then provide an algorithm for the satisfiability problem for \(K^{\#}\). In this article, we capture AC-GNN (aggregation-combination graph neural networks) [3] that are defined by an aggregation function which is the sum of feature vectors, the combination functions being linear functions truncated with the activation function \(max(0,min(1,x))\), and where the classification function is linear too. The \(max(0,min(1,x))\) is called truncated reLU (see [3]) or clipped reLU (see [22]).

The logic \(K^{\#}\) we consider is a combination of counting modalities and linear programming. It extends graded modal logic. We provide a translation from any GNN \(A\) to a formula \(tr(A)\) in \(K^{\#}\) so the problems P1-4 reformulate as follows:

* P1: is \(tr(A)\leftrightarrow\varphi\) valid?
* P2: is \(tr(A)\rightarrow\varphi\) valid?
* P3: is \(\varphi\to tr(A)\) valid?
* P4: is \(\varphi\wedge tr(A)\) satisfiable?

The formula \(\varphi\) can be for instance a formula of modal logic K and graded modal logic. As \(K^{\#}\) subsumes these logics, all the problems P1-4 in fact reduce to the satisfiability problem of \(K^{\#}\) (recall that a formula valid if its negation is unsatisfiable). We prove that the satisfiability problem of \(K^{\#}\) is _decidable_.

Interestingly, given a formula, we are able to construct an equivalent GNN. This can be used to _tune_ an existing GNN. Suppose you learnt a GNN \(A\) but you aim at constructing a new GNN that behaves like \(A\) but excludes the pointed graphs that do not satisfy \(\varphi\). More precisely, for the following problem:
**Tuning of a GNN** * input: a GNN \(A\), a logical formula \(\varphi\) * output: a new GNN \(A^{\prime}\) such that \([[A^{\prime}]]=[[A]]\cap[[\varphi]]\)

we simply take a GNN \(A^{\prime}\) that represents the formula \(tr(A)\wedge\varphi\). More precisely, the contributions of this paper are:

* the formal definition of logic \(K^{\#}\);
* the construction of a GNN \(A\) equivalent to a \(K^{\#}\)-formula \(\varphi\) (it generalizes the result of Prop 4.1 in [3])
* the construction of a \(K^{\#}\)-formula \(tr(A)\) equivalent to \(A\)
* the fact that the satisfiability problem of \(K^{\#}\) is in \(\mathsf{EXPTIME}^{\mathsf{NP}}\) (i.e. \(\mathsf{EXPTIME}\) with an \(\mathsf{NP}\) oracle).
* Restrictions of the satisfiability problem that are in \(\mathsf{PSPACE}\).

Outline.In Section 2 we recall the definition of AC-GNN. In Section 3, we define the logic \(K^{\#}\). In Section 4.1, we study the correspondence between GNN and logic \(K^{\#}\). In Section 5, we discuss the satisfiability problem of \(K^{\#}\).

## 2 Background on AC-GNN

In this paper, we consider aggregate-combine GNN (AC-GNN) [3], also sometimes called message passing neural network (MPNN) [8]. In the rest of the paper, we call a AC-GNN simply a GNN.

Definition 1 (labeled graph): A (labeled directed) graph \(G\) is a tuple \((V,E,\ell)\) such that \(V\) is a finite set of vertices, \(E\subseteq V\times V\) a set of directed edges and \(\ell\) is a mapping from \(V\) to a valuation over a set of atomic propositions. We write \(\ell(u)(p)=1\) when atomic proposition \(p\) is true in \(u\), and \(\ell(u)(p)=0\) otherwise.

Definition 2 (state): A state \(x\) is a mapping from \(V\) into \(\mathbb{R}^{d}\) for some \(d\).

As in [18], we use the term'state' for both denoting \(x\) and also the vector \(x(v)\) at a given vertex \(v\). Suppose that the relevant atomic propositions are \(p_{1},\ldots,p_{k}\). The initial state \(x_{0}\) is defined by:

\[x_{0}(u)=(\ell(u)(p_{1}),\ldots,\ell(u)(p_{k}),0,\ldots,0)\]

for all \(u\in V\). For simplicity, we suppose that all states are of the same dimension \(d\).

Definition 3 (aggregation function/combination function): An aggregation function \(AGG\) is a function mapping finite multisets of vectors in \(\mathbb{R}^{d}\) to vectors in \(\mathbb{R}^{d}\). A combination function \(COMB\) is a function mapping a vector in \(\mathbb{R}^{2d}\) to vectors in \(\mathbb{R}^{d}\).

Definition 4 (GNN layer): A GNN layer of input/output dimension \(p\) is defined by an aggregation function \(AGG\) and a combination function \(COMB\).
Definition 5 (Gnn): A GNN is a tuple \((\mathcal{L}^{(1)},...\mathcal{L}^{(L)},CLS)\) where \(\mathcal{L}^{(1)},...\mathcal{L}^{(L)}\) are \(d\) GNN layers and \(CLS:\mathbb{R}^{d}\rightarrow\{0,1\}\) is a classification function.

When applied to a graph \(G\), the \(t\)-th GNN layer \(\mathcal{L}^{(t)}\) transforms the previous state \(x_{t-1}\) into the next state \(x_{t}\) by:

\[x_{t}(u)=COMB(x_{t-1}(u),AGG(\{\{x_{t-1}(v)|uv\in E\}\}))\]

where \(AGG\) and \(COMB\) are respectively the aggregation and combination function of the \(t\)-th layer. In the above equation, note that the argument of \(AGG\) is the multiset of the state vectors of the successors of \(v\). Thus, the same vector may occur several times in that multiset. Figure 1 explains how a layer works at each vertex.

Figure 2 explains how the overall GNN works: the state is updated at each layer; at the end the fonction \(CLS\) says whether each vertex is positive (1) or negative (0).

Definition 6: Let \(A\) be GNN. We define \([[A]]\) as the set of pointed graphs \((G,u)\) such that \(CLS(x_{L}(u))=1\).

In the rest of the article, we suppose that the aggregation function is a sum:

\[AGG(X)=\sum_{x\in X}x.\]

Figure 1: A layer in a GNN transforms the state \(x_{t-1}\) at step \(t-1\) into the state \(x_{t}\) at time \(t\). The figure shows how \(x_{t}(u)\) is computed. First, the function \(AGG\) is applied to the state in the successors of \(u\). Then \(COMB\) is applied to that result and \(x_{t-1}(u)\) to obtain \(x_{t}(u)\).

Figure 2: General idea of a GNN with 2 layers applied on a graph with 4 vertices.
## 3 Our proposal: logic \(K^{\#}\)

In this section, we describe the syntax and semantics of \(K^{\#}\). We finish the section by defining its satisfiability problem.

### Syntax

Consider a countable set \(Ap\) of propositions. We define the language of logic \(K^{\#}\) as the set of formulas generated by the following BNF:

\[\varphi ::=p\mid\neg\varphi\mid\varphi\vee\varphi\mid E\geq 0\] \[E ::=c\mid 1_{\varphi}\mid\#\varphi\mid E+E\mid c\times E\]

where \(p\) ranges over \(Ap\), and \(c\) ranges over \(\mathbb{Z}\). This logic is an extension of modal logic. Atomic formulas are propositions \(p\), inequalities and equalities of linear expressions. We consider linear expressions over \(1_{\varphi}\) and \(\#\varphi\). The number \(1_{\varphi}\) is equal to \(1\) if \(\varphi\) holds in the current world and equal \(0\) otherwise. The number \(\#\varphi\) is the number of successors in which \(\varphi\) hold. The language seems strict but we write \(E_{1}\leq E_{2}\) for \(E_{2}-E_{1}\geq 0\), \(E=0\) for \((E\geq 0)\wedge(-E\geq 0)\), etc.

Example 1: Graded modal logic [6] extends classical modal logic by offering counting modality constructions of the form \(\diamond^{\geq k}\varphi\) which means there are at least \(k\) successors in which \(\varphi\) holds. Logic \(K^{\#}\) is more expressive than Graded modal logic since \(\diamond^{\geq k}\varphi\) is rewritten in \(k\leq\#\varphi\).

Example 2: Interestingly, the property 'there are more \(p\)-successors than \(q\)-successors' can be expressed in logic \(K^{\#}\) by \(\#p\geq\#q\), but cannot be expressed in FO, thus not graded modal logic. This is proven via a Ehrenfeucht-Fraisse game.

The set of subformulas, \(sub(\varphi)\) is defined by induction on \(\varphi\):

\[sub(p) =\{p\}\] \[sub(\neg\varphi) =\{\neg\varphi\}\cup sub(\varphi)\] \[sub(\varphi\vee\psi) =\{\varphi\vee\psi\}\cup sub(\varphi)\cup sub(\psi)\] \[sub(E\geq 0) =\{E\geq 0\}\cup\bigcup\{sub(\psi)\mid 1_{\psi}\text{ or }\#\psi\text{ appears in }E\}\]

The modal depth of a formula, \(md(\varphi)\) and the modal depth of an expression, \(md(E)\) are defined by mutual induction on \(\varphi\) and \(E\):

\[md(p) =0 md(c) =0\] \[md(\neg\varphi) =md(\varphi) md(1_{\varphi}) =md(\varphi)\] \[md(\varphi\vee\psi) =\max(md(\varphi),md(\psi)) md(\#\varphi) =md(\varphi)+1\] \[md(E\geq 0) =md(E) md(E_{1}+E_{2}) =max(md(E_{1}),md(E_{2}))\] \[md(k*E) =md(E)\]

As in modal logic, modalities are organized in levels.
Example 3: \(md((1_{p\wedge\#q\leq 4}\leq\#(\#p\geq 2)\leq 4)=2\). The expressions \(\#q\) and \(\#(\#p\geq 2)\) are at the root level (level 1), while the expression \(\#p\) is at level 2.

A formula can be represented by a DAG (directed acyclic graph) instead of just a syntactic tree. It allows to share common expressions. For instance \(\#(p\wedge q)\geq 1_{p\wedge q}\) is represented by the following DAG in which \(p\wedge q\) is used twice:

### Semantics

As in modal logic, a formula \(\varphi\) is evaluated in a pointed graph \((G,u)\) (also known as pointed Kripke model).

Definition 7: We define the truth conditions \((G,u)\models\varphi\) (\(\varphi\) is true in \(u\)) and the semantics \([[E]]_{G,u}\) (the value of \(E\) in \(u\)) of an expression \(E\) by mutual induction on \(\varphi\) and \(E\) as follows.

\[\begin{array}{ll}(G,u)\models p&\text{if }\ell(u)(p)=1\\ (G,u)\models\neg\varphi&\text{if it is not the case that }(G,u)\models\varphi\\ (G,u)\models\varphi\wedge\psi&\text{if }(G,u)\models\varphi\text{ and }(G,u)\models\psi\\ (G,u)\models E\geq 0&\text{if }[[E]]_{G,u}\geq 0\end{array}\]

\[\begin{array}{ll}[[c]]_{G,u}&=c\\ [[E_{1}+E_{2}]]_{G,u}&=[[E_{1}]]_{G,u}+[[E_{2}]]_{G,u}\\ [[c\times E]]_{G,u}&=c\times[[E]]_{G,u}\\ [[1_{\varphi}]]_{G,u}&=\begin{cases}1&\text{if }(G,u)\models\varphi\\ 0&\text{else}\end{cases}\\ [[\#\varphi]]_{G,u}&=|\{v\in V\mid(u,v)\in E\text{ and }(G,v)\models\varphi\}|\end{array}\]

Example 4: Consider the pointed graph \(G,u\) shown in Figure 3. We have \(G,u\models p\wedge(\#\neg p\geq 2)\wedge\#(\#p\geq 1)\leq 1\). Indeed, \(p\) holds in \(u\), \(u\) has (at least) two successors in which \(\neg p\) holds. Moreover, there is (at most) one successor which has at least one \(p\)-successor.

Definition 8: \([[\varphi]]\) is the set of the pointed graphs \(G,u\) such that \(G,u\models\varphi\).

Figure 3: Example of a pointed graph \(G,u\). We indicate true propositional variables at each vertex.
Definition 9: We say that \(\varphi\) is satisfiable when there exists a pointed graph \(G,u\) such that \(G,u\models\varphi\). The satisfiability problem is: given \(\varphi\) in the language of \(K^{\#}\), is \(\varphi\) satisfiable?

## 4 Correspondence

We explain how to transform a \(K^{\#}\)-formula into a GNN, and vice versa.

### From logic to GNN

Let us show that each \(K^{\#}\)-formula is captured by a GNN. The proof follows the same line that the proof of the fact that each formula of graded modal logic is captured by a GNN (see Prop 4.1 in [3]). However, our first result (point 1 in the following theorem) is a generalisation of their result since logic \(K^{\#}\) is more expressive than graded modal logic. Moreover, point 2 of the following theorem explicitly mentions a bound on the number of layers in the GNN.

Theorem 4.1: _For each \(K^{\#}\)-formula \(\varphi\), we can compute a GNN \(A\) such that \([[\varphi]]=[[A]]\). Furthermore, we have:_

1. _Either the number of layers and the dimension of the states in_ \(A\) _is_ \(|\varphi|\)_;_
2. _Or the number of layers of_ \(A\) _is_ \(O(md(\varphi))\)_._

Proof: Let \(\varphi\) be a \(K^{\#}\) formula. Let \((\varphi_{1},...\varphi_{L})\) be an enumeration of the sub-formulas of \(\varphi\) such that \(\varphi_{L}=\varphi\). We will construct a GNN \(\mathcal{A}_{\varphi}\) with \(L\) layers. The dimension of the states is \(L\). The goal is that for all \(k\leq n\), the \(k\)-th component of \(x_{\ell}(v)\) is equal to 1 if the formula \(\varphi_{k}\) is satisfied in node \(v\), or 0 otherwise. The aggregation and combination function in each layer are set by:

\[AGG(X) =\sum_{x\in X}\mathbf{x}\] \[COMB(x,y) =\boldsymbol{\sigma}(xC+yA+b)\]

where \(\boldsymbol{\sigma}\) is the function that applies componentwise the function \(\sigma(x)=min((max(0,x),1)\) and where \(A,C\in\mathbb{R}^{L\times L}\) and \(b\in\mathbb{R}^{L}\) are defined as follows. All cells are zeros, except the cells given in the following table:

\begin{tabular}{l l l} \(\varphi_{\ell}\) & \(\ell\)-th columns of \(C\) and \(A\) & \(b_{\ell}\) \\ \hline \(p\) & \(C_{\ell\ell}=1\) & 0 \\ \(\neg\varphi_{i}\) & \(C_{i\ell}=-1\) & 1 \\ \(\varphi_{i}\vee\varphi_{j}\) & \(C_{i\ell}=C_{j\ell}=1\) & 0 \\ \(\varphi_{i}\wedge\varphi_{j}\) & \(C_{i\ell}=C_{j\ell}=1\) & -1 \\ \(c\leq\sum_{i\in I}k_{i}\times 1_{\varphi_{i}}+\sum_{i\in I^{\prime}}k_{i}\times \#\varphi_{i}\) & \(C_{i\ell}=k_{i}\) for \(i\in I\) & \(-c+1\) \\  & \(A_{k\ell}=k_{i}\) for \(i\in I^{\prime}\) & \\ \end{tabular}
For proving point 2., the idea is to transform each propositional level of \(\varphi\) into a CNF. We obtain a \(K^{\#}\)-formula \(\varphi^{\prime}\) potentially exponentially larger than \(\varphi\).

The advantage is now that each propositional level is a CNF and thus is of depth at most 2. We treat an arbitrary large disjunction or conjunction as a single step of computation. In other words, we now consider an enumeration \((\varphi_{1},...\varphi_{L})\) of subformulas of \(\varphi^{\prime}\) such that \(\varphi_{L}=\varphi^{\prime}\) and with \(L=O(md(\varphi))\). Here are the corresponding \(\ell\)-columns of \(C\) and \(b_{\ell}\) for the cases where \(\varphi_{\ell}\) is an arbitrary large disjunction or conjunction:

\[\begin{array}{ll}\frac{\varphi_{\ell}}{\mbox{$\bigvee_{i\in I}\varphi_{i}^{ \prime\prime}\vee\bigvee_{i\in I^{\prime}}$}\,\neg\varphi_{i}^{\prime\prime} \ C_{i\ell}&b_{\ell}\\ \\ \bigwedge_{i\in I}\varphi_{i}^{\prime\prime}&C_{i\ell}&=1\,\mbox{for $i\in I $}&-card(I)+1\end{array}\]

Example 5: Consider the formula \(\varphi=p\wedge(8\leq 3\times\#q)\). We define the following GNN \(A\) which is equivalent to \(\varphi\) as follows. The aggregation function at each layer is \(AGG(X)=\sum_{x\in X}x\). The combination function for each layer is \(COMB(x,y)=\boldsymbol{\sigma}(xC+yA+b)\) where \(C=\begin{pmatrix}1&0&0&1\\ 0&1&0&0\\ 0&0&0&1\\ 0&0&0&0\end{pmatrix}\), \(A=\begin{pmatrix}0&0&0&0\\ 0&0&3&0\\ 0&0&0&0\\ 0&0&0&0\end{pmatrix}\), and \(b=\begin{pmatrix}0&0&-7&-1\end{pmatrix}\). The columns in the matrices (from top to bottom) are respectively evaluated the following subformulas in that order: \(p\), \(q\), \(8\leq\#q\), \(\varphi\).

### From GNN to logic

In this subsection, we show how to compute a \(K^{\#}\)-formula that is equivalent to a GNN. Note that this direction was already tackled for graded modal logic for the subclass of GNNs that are FO-expressible, but their proof is not constructive [3].

Theorem 4.2: _Let \(A\) be a GNN \(A\) with all aggregation function being \(AGG(X)=\sum_{x\in X}x\), and the classfication function being linear: \(CLS(x)=\sum_{i}a_{i}x_{i}\geq 0\). Then we can compute in poly-time in \(|A|\) a \(K^{\#}\)-formula \(tr(A)\) represented as DAG such that \([[A]]=[[tr(A)]]\)._

Proof: Let us consider a GNN \(A\) of \(L\) layers where the aggregation function is always: \(AGG(X)=\sum_{x\in X}\mathbf{x}\).

The idea is that we represent the state \(x_{0}(v)\) at all vertices \(v\) by the truth value of some formulas. Initially, the states is represented by the formulas \((p_{1},\ldots,p_{k},\bot,\ldots,\bot)\).

Suppose that states \(x_{t}(v)\) are represented by the formulas \((\varphi_{1},\ldots,\varphi_{d})\). Then if the combination function is \(COMB(x,y)=\boldsymbol{\sigma}(xC+yA+b)\) then the states \(x_{t+1}(v)\) are represented by the formulas \((\varphi_{1}^{\prime},\ldots,\varphi_{d}^{\prime})\) where \(\varphi_{\ell}^{\prime}\) is

\[\sum_{i=1..d}1_{\varphi_{i}}C_{i\ell}+\sum_{i=1..d}\#\varphi_{i}A_{i\ell}+b_{ \ell}\geq 1\]

Now, we have formulas \((\varphi_{1},\ldots,\varphi_{d})\) to represent \(x_{L}(v)\). As \(CLS\) is linear, the final formula is \(1_{CLS(\varphi_{1},\ldots,\varphi_{d})}\). \(CLS(x_{L}(u))=1\).
## 5 Decidability

Let us give an algorithm to solve the satisfiability of \(K^{\#}\), inspired by classical tableau method for modal logic K [7], but taking linear constraints into account.

### Design of the algorithm

First constructions \(1_{\psi}\) are easy to treat. Either \(\psi\) holds and we say that \(1_{\psi}=1\), or \(\psi\) does not hold and we say that \(1_{\psi}=0\). However, treating naively \(\#\psi\) as variables in a linear program will unfortunately not work. Let us note \(\#\psi_{1},\ldots\#\psi_{n}\) the variables of the form \(\#\psi\) that appear in \(\varphi\) and that are not in the scope of a \(\#\)-modality. First, some \(\psi_{i}\) may be unsatisfiable, thus \(\#\psi_{i}=0\). But the issue is more subtle. For instance, we always have \(\#p+\#\neg p=\#q+\#\neg q\) (1). The reader may imagine even more involved interactions between the \(\#\psi_{i}\) than equation (1). To take this interactions into account, we consider all possible conjunctions of \(\psi_{i}\) and \(\neg\psi_{i}\). We define for all words \(w\in\{0,1\}^{n}\):

\[conj_{w}:=\bigwedge_{i=1..n|w_{i}=1}\psi_{i}\wedge\bigwedge_{i=1..n|w_{i}=0} \neg\psi_{i}.\]

Example 6: \(conj_{0100}=\neg\psi_{1}\wedge\psi_{2}\wedge\neg\psi_{3}\wedge\neg\psi_{4}\).

We then introduce a variable in the linear program for each word \(w\) that counts the number of successors in which \(conj_{w}\) holds. We have \(\#\psi_{i}=\sum_{w|w_{i}=1}x_{w}\).

Example 7: How do we guarantee that \(\#p+\#\neg p=\#q+\#\neg q\)? Suppose that \(\psi_{1}=p,\psi_{2}=\neg p,\psi_{3}=q,\psi_{4}=\neg q\). As \(p\wedge\neg p\) is unsatisfiable, we have \(x_{1100}=x_{1101}=x_{1110}=x_{1111}=0\). We write \(x_{11**}=0\). In the same way, as and \(p\wedge\neg p\) and \(q\wedge\neg q\) are unsatisfiable \(x_{00**}=0\), \(x_{**00}=0\) and \(x_{**11}=0\). Finally:

\[\#p =x_{1010}+x_{1001} \#\neg p =x_{0110}+x_{0101}\] \[\#q =x_{1010}+x_{0110} \#\neg q =x_{1001}+x_{0101}\]

We see that \(\#p+\#\neg p=x_{1010}+x_{1001}+x_{0110}+x_{0101}=\#q+\#\neg q\).

Instead of providing tableau rules, we decided to present a more abstract version with Hintikka sets (see Def. 6.24 in [4]). They can be thought as a possible way to completely apply Boolean rules while keeping consistent. We adapt the definition to our setting.

Definition 10 (Hintikka set): A Hintikka set \(\Sigma\) for formula \(\varphi\) is a smallest (for inclusion) set of subformulas such that:

1. \(\varphi\in\Sigma\);
2. if \(\psi_{1}\wedge\psi_{2}\in\Sigma\) then \(\psi_{1}\in\Sigma\) and \(\psi_{2}\in\Sigma\)
3. if \(\psi_{1}\vee\psi_{2}\in\Sigma\) then \(\psi_{1}\in\Sigma\) or \(\psi_{2}\in\Sigma\)
4. for all \(\psi\), \(\psi\not\in\Sigma\) or \(\neg\psi\not\in\Sigma\)
5. \(1_{\psi}\) appears in \(\varphi\), either \(\psi\in\Sigma\) and \(1_{\psi}=1\in\Sigma\), or \(\neg\psi\in\Sigma\) and \(1_{\psi}=0\in\Sigma\).
Point 1 says that \(\varphi\) should be true. In point 3, if \(\psi_{1}\vee\psi_{2}\) then one of the formula - \(\psi_{1}\) or \(\psi_{2}\) - should be true, without telling which one. Point 4 is the consistency. Point 5 makes the link between the truth of \(\psi\) and the value of \(1_{\psi}\).

Example 8: Consider formula \(\varphi=p\wedge(\#r\geq 1_{q})\). There are two possible Hintikka sets for formula \(\varphi\): \(\{p,\#r\geq 1_{q},1_{q}=1,q\}\) and \(\{p,\#r\geq 1_{q},1_{q}=0,\neg q\}\).

The algorithm (see Figure 4) consists in examining all possible Hintikka sets. For each of them, we extract the linear program (line 3). We then compute the integer linear program by considering the variables \(x_{w}\) discussed above (line 6). Line 7: we call recursively the function sat on \(conj_{w}\) and we add the constraint \(x_{w}=0\) in case \(conj_{w}\) is unsatisfiable.

### Soundness and completeness

Proposition 1: \(\varphi\) _is \(K^{\#}\)-satisfiable iff \(sat(\varphi)\) returns true._

Proof: We prove the proposition by induction on \(md(\varphi)\). The induction works because \(md(conj_{w})<md(\varphi)\). Suppose that \(\varphi\) is satisfiable: let \(G,v\) such that \(G,u\models\varphi\). Let us prove that \(sat(\varphi)\) returns true. We consider the Hintikka set \(H\) made up of formulas that are true in \(G,v\). The obtained \(S\) is ILP-satisfiable because these equations and inequations are satisfied in \(G,u\). Indeed, here is a solution: we set \(x_{w}\) to be the number of successors of \(u\) in which \(conj_{w}\) hold. By induction, the call \(sat(conj_{w})\) are all correct: so if \(sat(conj_{w})\) returns false, then \(conj_{w}\) is unsatisfiable. Thus there are no \(u\)-successors satisfying \(conj_{w}\), and the constraints \(x_{w}=0\) (added line 8) hold. The number of \(v\)-successors satisfying \(\psi_{i}\) is \(\sum_{w|w_{i}=1}x_{w}\). So \(S\) is ILP-satisfiable, and the algorithm returns true.

Conversely, suppose that \(sat(\varphi)\) returns true. First, consider \(S\) the corresponding Hintikka set for which the algorithm returned true. From \(S\) we extract a valuation \(\ell(u)\) for the propositions to be set to true or false at a node \(u\). By induction, for all \(w\in\{0,1\}^{n}\), the call \(sat(conj_{w})\) are all correct. Thus, if \(conj_{w}\) is unsatisfiable, \(x_{w}=0\); otherwise \(x_{w}\) is not constrained. As \(sat(\varphi)\) returned true,

Figure 4: Algorithm for checking the satisfiability of a \(K^{\#}\)-formula \(\varphi\).
we know that \(S\) is ILP-satisfiable. Consider a solution. If \(x_{w}>0\), we know that \(conj_{w}\) is satisfiable. We consider \(x_{w}\) copies of a pointed graph \(G_{w},u_{w}\) satisfying \(conj_{w}\). We construct a model \(G,u\) for \(\varphi\) as follows. We take \(u\) as the point with valuation \(\ell(v)\). We then link \(u\) to each point of the copies of \(u_{w}\). The inequations in \(S\) are satisfied at \(G,u\). Indeed, the \(u\)-successors satisfying \(\psi_{i}\) are exactly the \(u_{w}\) with \(w_{i}=1\), and \(\#\psi_{i}\) is \(\sum_{w|w_{i}=1}x_{w}\). Thus, the obtained pointed \(G,u\) is a model of \(\varphi\). Figure 5 shows an example of the construction.

Note that \(K^{\#}\) has the tree-model property as modal logic K. It can be proven by induction on \(md(\varphi)\), relying on the construction in the \(\Leftarrow\)-direction in the proof above.

### Complexity

The recursive depth of our algorithm (Figure 4) is bounded by the modal depth \(md(\varphi)\) of the initial formula \(\varphi\): the recursive tree is of depth \(md(\varphi)\). Its branching factor is exponential in \(|\varphi|\). The number of nodes remains exponential in \(|\varphi|\). At each node, there is an exponential number of steps, provided that the ILP-solver is considered as an NP-oracle since integer linear programming (ILP) is in NP [13] (note that the linear programs computed here are of exponential size in \(|\varphi|\)). Our algorithm runs in exponential time in \(|\varphi|\), by calling a NP-oracle: deciding the satisfiability problem of \(K^{\#}\) is in \(\mathsf{EXPTIME}^{\mathsf{NP}}\). The class \(\mathsf{EXPTIME}^{\mathsf{NP}}\) is defined as the class of decision problems decided by an algorithm running in exponential time (i.e. \(2^{poly(n)}\)) with a NP oracle, typically a SAT oracle or a ILP oracle (note that exponentially long ILP instances may be solved in one step) (see [23], [10]). Note that the complexity class \(\mathsf{EXPTIME}^{\mathsf{NP}}\) is included in the exponential hierarchy which is included in \(\mathsf{EXPSPACE}\).

Theorem 5.4: _The satisfiability problem of \(K^{\#}\) is decidable and is in \(\mathsf{EXPTIME}^{\mathsf{NP}}\)._

### \(\mathsf{PSPACE}\) subcases

Let us discuss three types of restrictions to get \(\mathsf{PSPACE}\)-membership.

Bounding the number of \(conj_{w}\).If we can limit the number of considered conjonctions \(conj_{w}\), we may obtain a procedure running in polynomial space, making the restricted version of the satisfiability problem of \(K^{\#}\) in \(\mathsf{PSPACE}\). For instance, if we know in advance that at each level of modal depth formulas in
the scope of a #-modality are mutually unsatisfiable, then we do not need to consider all the conjunctions \(conj_{w}\): all \(conj_{w}\) are 0 except \(conj_{10\ldots 0}\), \(conj_{010\ldots 0}\), \(...\), \(conj_{0\ldots 01}\). We keep a linear program polynomial in \(|\varphi|\).

Bounded the number of modalities.If we artificially make the syntactic restriction where we bound the number \(n\) of #\(\varphi\) at each level, the satisfiability problem is also in \(\mathsf{PSPACE}\). Indeed, \(n\) becomes a constant, thus \(2^{n}\) is a constant too. The size of \(S\) is only polynomial in the size of \(\varphi\).

Bounded branching.Many graphs have bounded branching: grid graphs (of degree 4), sparse networks, etc. If we ask whether a formula is satisfiable in a graph whose degree is bounded by a polynomial in the size of the input, then only a polynomial number of variables \(x_{w}\) will be non-zero. The algorithm is then adapted by guessing the polynomial-size subset of variables \(x_{w}\) that are non-zero. Again, we can run the algorithm in polynomial space.

Proposition 2: _Let \(k>0\) be an integer. The satisfiability problem of \(K^{\#}\) restricted to graphs of degree at most \(k\) is \(\mathsf{PSPACE}\)-complete._

Proof: \(\mathsf{PSPACE}\)-membership comes from the discussion above. \(\mathsf{PSPACE}\)-hardness holds because the modal logic on graphs with at most 2 successors per worlds is \(\mathsf{PSPACE}\)-hard. Write \(\Box\psi\) as #\(\neg\psi\leq 0\).

Interestingly, there are fragments in which if a formula \(\varphi\) is satisfiable then \(\varphi\) is satisfiable in a model of polynomial degree in \(|\varphi|\). Consider the fragment in which inequalities in formulas are of the form #\(\psi\leq\)#\(\psi^{\prime}\) (i.e. no addition, no multiplication by a scalar). Then if there is a solution, we can at each level have an ordering #\(\psi_{1}\leq\cdots\leq\#\psi_{n}\) where some of the \(\leq\) may be strict. But then we can suppose that w.l.o.g. \(0\leq\)#\(\psi_{i+1}-\#\psi_{i}\leq 1\). It means that the number of successors of each \(\psi_{i}\) is \(O(i)\); the number of successors is \(O(n^{2})\). We get:

Proposition 3: _The satisfiability problem of \(K^{\#}\) is \(\mathsf{PSPACE}\)-complete when inequalities in formulas are of the form #\(\psi\leq\)#\(\psi^{\prime}\)._

Proof: \(\mathsf{PSPACE}\)-membership comes from the discussion above. \(\mathsf{PSPACE}\)-hardness comes from the fact modal logic K is reducible to it. Write \(\Box\psi\) as #\(\top\)\(\leq\)#\(\psi\).

## 6 Related work

Many works combine modal logic and quantitative aspects: counting ([1], [9]), probabilities [20]. Linear programming and modal logic have already been combined to solve the satisfiability problem of graded/probabilistic modal logic [21]. Our logic \(K^{\#}\) can be seen as a'recursification' of the logic used in [17]. They allow for counting successors satisfying a given feature, and not any subformula. Interestingly, they allow for counting also among all nodes in the graph (sort of counting universal modality). Their logic is proven to be undecidable by reduction from the Post correspondence problem. Contrary to our setting, they use
their logic only to characterize labelled graphs, but not to give a back and forth comparison with the GNN machinery itself.

Modal logic has also been combined with neural network in the so-called _Connectionist modal logic_[5] but it has no direct connection with GNNs.

Another solution would be to use directly explainable GNN such as those in [12]. This is of course a deep debate: using models easy to use for learning, versus interpretable models [15]. The choice depends on the target application.

Yuan et al. [24] provide a survey on methods used to provide explanations for GNNs by using black-box techniques. According to them, they are instance-level and model-level explanations. Instance-level explanations explain on why a graph has been recognized by an GNN; model-level ones how a given GNN works. For instance, they are also many methods based on Logic Explained Networks and variants to generate logical explanation candidates \(\varphi\)[2]. Once a candidate is generated we could imagine use our problem P1 (given in the introduction) to check whether \([[A]]=[[\varphi]]\), and thus being able to fully synthesize a trustworthy explanation. Our paper is clearly close to model-level explanations.

## 7 Perspectives

We aim at considering a larger class of GNNs. This will need to augment the expressivity of the logic, for instance by adding reLU in the language. Fortunately SMT solvers have been extended to capture reLU [11].

Another possible direction would be to consider other classes of graphs. For instance, reflexive, transitive graphs. Restricted types of graphs lead to different modal logics: \(KT\) (validities on reflexive Kripke models), \(KD\) (on serial models), \(S4\) (reflexive and transitive models), \(KB\) (models where relations are symmetric), \(S5\) (models where relations are equivalence relations), etc. [4] The logic \(K^{\#}\) defined in this paper is the counterpart of modal logic K with linear programs. In the same way, we could define \(KT^{\#}\), \(S4^{\#}\), \(S5^{\#}\), etc. For instance, \(KB^{\#}\) would be the set of validities of \(K^{\#}\)-formulas over symmetric models; \(KB^{\#}\) would be the logic used when GNNs are only used to recognize undirected pointed graphs (for instance persons in a social network where friendship is undirected). In the future work, some connections between GNNs and logics designed to express properties over persons in social network, such as [19] could be investigated.

A next direction of research would be to build a tool. The main difficulty is the complexity of the algorithm. However, we may rely on heuristics to guide the search (namely SAT solvers for computing only the relevant Hintikka sets, and relaxed linear programs). We could also directly use SMT solvers.

Of course, our Saint-Graal is the synthesis of a formula that matches a specification. This problem is close to the formula synthesis problem presented in [14]. An idea would be to represent the set of possible suitable explanation formulas by a grammar \(G\) (for instance, the grammar restricted to graded modal logic) and to compute a formula generated by \(G\) which is equivalent to \(tr(A)\).