A Logic for Reasoning about Aggregate-Combine Graph Neural Networks

1 Introduction

Graph Neural Networks (GNNs) perform computations on graphs or on pairs of graphs and vertices, referred to as pointed graphs. As a prominent deep learning model, GNNs find applications in various domains such as social recommendations [Salamat et al., 2021], drug discovery [Xiong et al., 2021], material science and chemistry [Reiser et al., 2022], knowledge graphs [Ye et al., 2022], among others (see Zhou et al. [2020] for an overview). This growing adoption of GNNs comes with certain challenges. The use of GNNs in safety-critical applications sparks a significant demand for safety certifications, given by dependable verification methods. Furthermore, human understandable explanations for the behaviour of GNNs are needed in order to build trustworthy applications, coming with the need for a general understanding of the capabilities and limitations inherent in specific GNN models.

In general, there are two approaches enabling rigorous and formal reasoning about GNNs: formal verification [Huang et al., 2020] and formal explanation methods [Marques-Silva and Ignatiev, 2022] for neural network models such as GNNs. Formal verification procedures are usually concerned with the sound and complete verification of properties like "Does GNN A produce an unwanted output y in some specified region Y ?" (reachability) or "Does GNN A behave as expected on inputs from some specified region X?" (robustness). Formal explainability methods are concerned with giving answers for questions like "Is there a minimal, humanly interpretable reason that GNN A produces output y given some input x?" (abductive explanations). In both cases, formal verification and formal explanation, logical reasoning offers an all-purpose tool. For example, the following algorithm enables addressing correspondence questions: given some GNN A, produce a logical formula ϕ such that [[A]] = [[ϕ]] where [[A]] is the class of (pointed) graphs recognized by the GNN A, and [[ϕ]] is the class of pointed graphs in which ϕ holds. Informally put, the goal is to compute a formula ϕ that completely characterizes the class of (pointed) graphs recognized by GNN A. Given this, one can then investigate GNNs purely based on this logical characterization. Unfortunately, the synthesis of a formula of a logic, say first-order logic (FO) or modal logic (ML), that captures a semantic condition can be notoriously challenging (e.g., Pinchinat et al. [2022]).

Barceló et al. [2020] have shown that any formula of Graded Modal Logic (GML) can be transformed into a GNN. Conversely, they have shown that given a GNN that is expressible in first-order logic (FO), there exists an equivalent formula in GML. Doing so, they also characterized GML as being the intersection of FO and GNNs. While their result is promising, there is no full logical characterization of what a GNN can express.

That is why we define a logic called K# combining counting modalities and linear programming, which is expressive enough to capture a broad and natural class of GNNs. As pictured in Figure 1, it is more expressive than graded modal logic [de Rijke, 2000] and, thus, K# captures a broader class of GNNs than previously identified in Barceló et al. [2020]. Furthermore, we show that the satisfiability problem of K# is PSPACE-complete, leading to immediate complexity results for various formal verification and explainability problems as reachability, robustness, or producing abductive explanations.

Overview of the Main Contributions. We present the logic K# which captures Aggregate-Combine Graph Neural Networks, also called Message Passing Neural Networks [Barceló et al., 2020; Gilmer et al., 2017], where the aggregation function is the sum, the combination and final classification functions are linear functions with integer parameters, and truncated ReLU (max(0,min(1, x))) is used for the activation function. We refer to these GNNs simply as GNNs in the paper. In particular, we show that:

• for each formula ϕ of K# there is a GNNA recognizing exactly the same pointed graphs as ϕ (Theorem 1),
• for eachGNNA there is a formula ϕ of K# recognizing exactly the same pointed graphs as A (Theorem 2).

These results significantly extend the class of GNNs for which a logical characterization is known from Barceló et al. [2020]. Furthermore, we provide an algorithm for the satisfiability problem of K#, proving that the problem is PSPACE-complete (Theorem 3). This also provides algorithmic solutions for the following problems: given a GNN A and a logical formula ϕ, decide whether (P1) [[A]] = [[ϕ]], (P2) [[A]] ⊆ [[ϕ]], (P3) [[ϕ]] ⊆ [[A]], (P4) [[ϕ]] ∩ [[A]] ̸= ∅.

Example 1. Consider a setting where GNNs are used to classify users in a social network. Assume we have a GNN A which is intended to recommend exactly those users who have at least one friend who is a musician and at most one-third of their friends play the tuba. We call this the few-tubas property. Given our translation from A to a K# formula, we can answer questions like

• A "Is each recommended person a person that has the fewtubas property?"
• B "Does any recommended person not have the few-tubas property?"
• C "Is any person that befriends a musician but also too many tuba players recommended?"
• D "Is it possible to recommend a person that does not have the few-tubas property?"

by representing the corresponding properties as K# formulas and then solving problem P1 for A, P2 for B, P3 for C and P4 for D. Question A corresponds to giving an abductive explanation, as a positive answer would indicate that "at least one musician friend and not too many tuba playing friends" is a (minimal) reason for "recommended person". In the same manner, B and C are reachability properties and D is a robustness property.

Outline. In Section 2 we recall the necessary preliminaries on graph neural networks. In Section 3, we define the logic K#. In Section 4, we study the correspondence between GNNs and K#. In Section 5, we discuss the satisfiability problem of K#. Section 6 addresses the complexity of the problems P1-P4. Section 7 is about the related work, and Section 8 concludes.

2 Background on GNNs

In this paper, we consider Aggregate-Combine GNNs (ACGNN) [Barceló et al., 2020], also sometimes called message passing neural networks [Gilmer et al., 2017].

An aggregation function agg is a function mapping finite multisets of vectors in Rd to vectors in Rd . A combination function comb is a function mapping a vector in R2d to vectors in Rd′ . An AC-GNN layer L of input dimension d is defined by an aggregation function agg and a combination function comb of matching dimensions, meaning agg expects and produces vectors from Rd and comb has input dimensionality 2d. The output dimension of L is given by the output dimension of comb. Then, an AC-GNN is a tuple (L(1) , . . . , L(L) , cls) where L(1) , . . . , L(L) are L AC-GNN layers and cls : Rd → {0, 1} is a classification function. We assume that all GNNs are well-formed in the sense that output dimension of layer L(i) matches input dimension of layer L(i+1) as well as output dimension of L(L) matches input dimension of cls.

Definition 1. Here we call a GNN an AC-GNN A where all aggregation functions are given by agg(X) = ∑x∈X x, all combination functions are given by comb(x, y) = ⃗σ(xC + yA+ b) where ⃗σ(x) is the componentwise application of the truncated ReLU σ(x) = max(0, min(1, x)), where C and A are matrices of integer parameters and b is a vector of integer parameters, and where the classification function is cls(x) = ∑i aixi ≥ 1, with ai integers.

A (labeled directed) graph G is a tuple (V, E, ℓ) such that V is a finite set of vertices, E ⊆ V ×V a set of directed edges and ℓ is a mapping from V to a valuation over a set of atomic propositions. We write ℓ(u)(p) = 1 when atomic proposition p is true in u, and ℓ(u)(p) = 0 otherwise. Given a graph G and vertex u ∈ V , we call (G, u) a pointed graph.

Let G = (V,E, ℓ) be a graph. A state x is a mapping from V into Rd for some d. When applied to a graph G, the t-th GNN layer L(t) transforms the previous state xt-1 into the next state xt. Supposing that the atomic propositions occurring in G are p1, . . . , pk, the initial state x0 is defined by:

for all u ∈ V . Then:

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 feature vectors of the successors of v. Thus, the same vector may occur several times in that multiset. Figure 2 explains how a layer works at each vertex.

Example 2. Consider a layer defined by agg(X) := ∑x∈X x and

Suppose as in Figure 2, that vertex u has two successors named v and w. Here we suppose that feature vectors are of dimension 2: xt-1(u), xt-1(v), xt-1(w) ∈ R2 . First, agg({{xt-1(v), xt-1(w)}}) = xt-1(v) + xt-1(w). Second, with our example of combination function we get:

Figure 3 explains how a GNN works overall: the state is updated at each layer; at the end the function cls says whether each vertex is recognized (output 1) or not (output 0).

Let A = (L(1) , . . . , L(L) , cls) be a GNN. We define the semantics [[A]] of A as the set of pointed graphs (G, u) such that cls(xL(u)) = 1.

3 The Logic K#

In this section, we describe the syntax and semantics of K# and its fragment K#,-1 .

3.1 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:

where p ranges over Ap, and c ranges over Z. Atomic formulas are propositions p, inequalities and equalities of linear expressions. We consider linear expressions over 1ϕ and #ϕ. The number 1ϕ is equal to 1 if ϕ holds in the current world and equal 0 otherwise. The number #ϕ is the number of successors in which ϕ hold. The language seems strict but we write ξ1 ≤ ξ2 for ξ2 - ξ1 ≥ 0, ξ = 0 for (ξ ≥ 0) ∧ (-ξ ≥ 0), etc. Recall that modal logic itself extends propositional logic with a modal construction □ϕ whose semantics is 'the formula holds in all successors'. Logic K# is an extension of modal logic since we can define □ϕ := (#(¬ϕ) ≤ 0): the number of successors in which ϕ does not hold equals 0. We write ⊤ for a tautology.

Example 3. The few-tuba property of Example 1, users (nodes) who have at least one friend who is a musician and at most one-third of their friends play the tuba, can be represented by the formula (#musician ≥ 1) ∧ (#⊤ ≥ 3 × #tubaplayer).

The set of subformulas, sub(ϕ) is defined by induction on ϕ: sub(p) = {p}, sub(¬ϕ) = {¬ϕ} ∪ sub(ϕ), sub(ϕ ∨ ψ) = {ϕ ∨ ψ} ∪ sub(ϕ) ∪ sub(ψ), and sub(ξ ≥ 0) = {ξ ≥ 0} ∪ ⋃{sub(ψ) | 1ψ or #ψ in ξ}.

The modal depth of a formula, md(ϕ) and the modal depth of an expression, md(ξ) are defined by mutual induction on ϕ and ξ: md(p) = md(c) = 0, md(¬ϕ) = md(1ϕ) = md(ϕ), md(ξ ≥ 0) = md(k · ξ) = md(ξ), md(#ϕ) = md(ϕ) + 1, and md(ξ1 + ξ2) = max(md(ξ1),md(ξ2)). As in modal logic, modalities are organized in levels.

Example 4. md(1p∧#q≤4 ≤ #((#p ≥ 2) ≤ 4)) = 2. The expressions #q and #(#p ≥ 2) are at the root level (level 1), while the expression #p is at level 2.

In this paper, a formula is represented by a DAG (directed acyclic graph) instead of just a syntactic tree. DAGs, contrary to syntactic trees, allow the reuse of subformulas.

Example 5. The DAG depicted in Figure 4(a), in which the subformula p ∧ q is used thrice, represents the formula (p ∧ q) ∨ (#(p ∧ q) ≥ 1p∧q).

However, we disallow DAGs reusing arithmetic expressions.

Example 6. The formula (2 +#p ≥ 1q) ∧ (2 +#p ≥ 1r) cannot be represented by the DAG shown in Figure 4(b) which refers to the expression 2 +#p twice.

Formally, the fact that arithmetic expressions are not reused in DAGs representing formulas is reflected by the simple property that the nodes representing arithmetical expressions have in-degree 1.

Definition 2. A DAG of a formula is a graph in which nodes for c, 1ϕ, #ϕ, ξ + ξ ′ , c × ξ have in-degree 1.

The reason for not allowing reusing arithmetical expressions in the DAG representation of formulas is technical. Firstly, as demonstrated by Theorem 2, the transformation of GNNs into formulas does not necessitate the reusing of arithmetical subexpressions but only subformulas. Second, we will need to efficiently transform formulas in DAG representation into formulas in tree representation (Lemma 1). For this result, we need DAGs wherein only subformulas are reused, excluding the reuse of arithmetical expressions. The size |ϕ| of a K# formula ϕ in DAG form is the number of bits needed to represent the DAG.

The logic K#,-1 is the syntactic fragment of K# in which constructions 1ϕ are disallowed.

3.2 Semantics

As in modal logic, a formula ϕ is evaluated in a pointed graph (G, u) (also known as pointed Kripke model). We define the truth conditions (G, u) |= ϕ (ϕ is true in u) by

and the semantics [[ξ]]G,u (the value of ξ in u) of an expression ξ by mutual induction on ϕ and ξ as follows.

We illustrate it in the next example.

Example 7. Consider the pointed graph G, u shown in Figure 5. We have G, u |= p ∧ (#¬p ≥ 2) ∧ #(#p ≥ 1) ≤ 1. Indeed, p holds in u, u has (at least) two successors in which ¬p holds. Moreover, there is (at most) one successor which has at least one p-successor.

We define [[ϕ]] as the set of the pointed graphs G, u such that G, u |= ϕ. Furthermore, we say that ϕ is satisfiable when there exists a pointed graph G, u such that G, u |= ϕ.

Definition 3. The satisfiability problemof K# (resp. K#,-1 ) is: given a DAG representation of a formula ϕ in the language of K# (resp. K#,-1 ), is ϕ satisfiable?

3.3 Relationship with Other Logics

Logic K# is also an extension of graded modal logic. Graded modal logic [Fattorosi-Barnaba and Caro, 1985] extends classical modal logic by offering counting modality constructions of the form ♦≥k ϕ which means there are at least k successors in which ϕ holds. Logic K# is more expressive than graded modal logic since ♦≥k ϕ is rewritten in k ≤ #ϕ. In fact, the expressivity of K# goes beyond FO.

Proposition 1. There are some properties that can be expressed in K# that cannot be expressed in FO.

Proof. The property 'there are more p-successors than qsuccessors' can be expressed in logic K# by the formula #p ≥ #q, but cannot be expressed in first-order logic, and thus not in graded modal logic. This is proven via an Ehrenfeucht-Fraïssé game (see [Nunn et al., 2024]).

4 Correspondence

In this section, we lay the foundations for expressing K#- formulas using GNNs, and vice versa.

4.1 FromLogic to GNNs

We start by showing that each K#-formula is captured by some GNN. The proof follows the same line as Prop 4.1 in Barceló et al. [2020]). However, our result is a generalization of their result since K# is more expressive than graded modal logic.

Theorem 1. For every K#-formula ϕ, we can compute in polynomial time wrt. |ϕ| a GNN Aϕ such that [[ϕ]] = [[Aϕ]].

Proof. Let ϕ be a K# formula with occurring propositions p1, . . . , pm. Let (ϕ1, . . . , ϕn) be an enumeration of the subformulas of ϕ such that ϕi = pi for all i ≤ m, if ϕi ∈ sub(ϕj) then i ≤ j and ϕn = ϕ. W.l.o.g. we assume that all ξ ≥ 0 subformulas are of the form ∑j∈J kj × 1ϕj + ∑j ′∈J ′ kj ′ × #ϕj ′ - c ≥ 0 for some index sets J, J ′ ⊆ {1, . . . , n}. We build Aϕ in a stepwise fashion. Since Aϕ is a GNN it is completely defined by specifying the combination function combi for each layer li with i ∈ {1, . . . , n} of Aϕ as well as the classification function.

The output dimensionality of each combi is n. Let comb1, namely the first combination in Aϕ, have input dimensionality 2m computing comb1(x, y) = (x, 0, . . . , 0). Informally, this ensures that state x1 has dimensionality n where the first m dimensions correspond to the propositions pi and all other are 0. Let combi(x, y) = ⃗σ(xC + yA + b) where C, A are n × n and b is n dimensional and specified as follows. All cells of C, A and b are zero except for the case Cii = 1 if i ≤ m, the case Cji = -1, bi = 1 if ϕi = ¬ϕj, the case Cji = Cli = 1 if ϕi = ϕj ∨ ϕl and the case Cji = kj,Aj ′ i = kj ′ , bi = -c + 1 for all j ∈ J, j ′ ∈ J ′ if ϕi = ∑j∈J kj × 1ϕj + ∑j ′∈J ′ kj ′ × #ϕj ′ ≥ c. This means that all combi are equal. The classification function cls is given by cls(x) = xn ≥ 1.

The correctness of the construction is proven in [Nunn et al., 2024].

Furthermore, the number of layers of an equivalent GNN can be reduced to be proportional to md(ϕ). In that case, however, the corresponding transformation is a priori not computable in poly-time (see [Nunn et al., 2024]).

The combination function for both layers is comb(x, y) = ⃗σ(xC + yA + b) where

The role of the two first column coordinates are to keep the current values of p and q in each vertex of the graph (hence the identity submatrix in C wrt the first two columns and rows).

The third column is about subformula 8 ≤ 3 ×#q. The coefficient 3 in A is at the second row (corresponding to q). The third column of xC + yA + b is equal to 3 × number of q-successors-7. The third column of ⃗σ(xC+yA+ b) equals 1 exactly when 3×number of q-successors-7 ≥ 1, i.e. exactly when 8 ≤ 3×#q should hold. The fourth column handles the disjunction of ϕ1 ∨ϕ3, hence the 1 in the first and third rows. The fourth column of ⃗σ(xC+yA+b) is σ(x1+x3) and equals 1 iff x1 = 1 or x3 = 1. The last column handles the negation ¬ϕ4. The last column of ⃗σ(xC + yA + b) is σ(1 - x4).

4.2 FromGNNs to Logic

Now, we shift our attention to show how to compute a K#- formula that is equivalent to a GNN. Note that this direction was already tackled by Barceló et al. [2020] for graded modal logic for the subclass of GNNs that are FO-expressible, but their proof is not constructive. Here we give an effective construction. Furthermore, the construction can be done in poly-time in |A|. This point is crucial: it means that we can transform efficiently a GNN into a logical formula and then perform all the reasoning tasks in the logic itself.

Theorem 2. Let A be a GNN. We can compute in polynomial time wrt. |A| a K#-formula ϕA, represented as a DAG, such that [[A]] = [[ϕA]].

Proof. Let A be a GNN with layers l1, . . . , lk where combi has input dimensionality 2mi, output dimensionality ni and parameters Ci, Ai and bi and cls(x) = a1x1+· · ·+ank xnk ≥ 1. We assume that mi = ni-1 for i ≥ 2, meaning a well defined GNN. We build a formula ϕA over propositions p1, . . . , pm1 inductively as follows. Consider layer l1. We build formulas ϕ1,j = ∑m1 k=1 1pk (C1)kj + #pk(A1)kj + bj ≥ 1 for each j ∈ {1, . . . , n1}. Now, assume that ϕi-1,1, . . . , ϕi-1,ni-1 are given. Then, we build formulas ϕi,j = ∑mi k=1 1ϕi-1,k Ckj+#ϕi-1,kAkj+bj ≥ 1. In the end,

we set ϕA = 1ψ where ψ = a11ϕk,1 + · · · + ank 1ϕk,nk ≥ 1.

Let G, v be some pointed graph. The correctness of our construction is straightforward: due to the facts that all parameters in A are from Z, the value x0(u) for each u in G is a vector of 0 and 1 and that each combi in A applies the truncated ReLU pointwise, we have for all i ∈ {1, . . . , k} that the value of xi(v) is again a vector of 0 and 1. Therefore, we can capture each xi using a sequence of K#-formulas as done above. In combination, we have that ϕA exactly simulates the computation of A.

The polynomial time of this inductive construction is straightforward: we represent from beginning to end the inductively built (sub)formulas in form of a single DAG. This implies that in intermediate steps we do not have to rewrite already built subformulas ϕi-1,k, but can simply refer to them. Thus, in each step of the inductive procedure we only need ni · mi many steps to build all corresponding subformulas. As all ni,mi and k are given by A, we have that the procedure is polynomial in the size of A as long as we represent ϕA respectively its subformulas as a DAG.

Example 9. The idea is to build formulas that characterize the state xt (which is the output at layer t if t ≥ 1, and also the input at layer t+1). Initially, x0 is the state whose values comes the truth values of the atomic propositions. We suppose we have only two propositions p1, p2. Hence, the two formulas that represent state x0 are ϕ01 = p1 and ϕ02 = p2. Suppose that the two layers are given by the same combination and aggregation functions:

with aggregation function agg(X) = ∑x∈X x, and combination function

The formulas that represent the state x1 are formula ϕ11 = 1ϕ01 + 2 × 1ϕ02 - 3#ϕ01 + 4#ϕ02 + 5 ≥ 1 and formula ϕ12 = 6 × 1ϕ01 + 7 × 1ϕ02 + 8#ϕ01 - 9#ϕ02 + 10 ≥ 1. The formulas that represent the state x2 are formula ϕ21 = 1ϕ11 + 2 × 1ϕ12 - 3#ϕ11 + 4#ϕ12 + 5 ≥ 1 and formula ϕ22 = 6 × 1ϕ11 + 7 × 1ϕ12 + 8#ϕ11 - 9#ϕ12 + 10 ≥ 1.

Finally, suppose that the classification function is given by cls(x, x′ ) = 5x - 3x′ ≥ 1. So the formula tr(A) that represents the GNN A is 5 × 1ϕ21 - 3 × 1ϕ22 ≥ 1.

5 Complexity of the Logic

In this section, we address the complexity of the satisfiability problem of the logic K#. Specifically, we prove that it is PSPACE-complete (Theorem 3). Additional details are available in [Nunn et al., 2024].

We know from Ladner [1977] that the satisfiability problem of the standard modal logic K is PSPACE-hard, and we observed before that K# is an extension of logic K since we can define □ϕ := (#(¬ϕ) ≤ 0) and we are working with graphs whose relation (represented by the set E of edges) is unconstrained. Hence, we have:

Proposition 2. The satisfiability problem of the logic K# is PSPACE-hard.

To show that the satisfiability problem of K# is also in PSPACE, we are going to follow a strategy illustrated in Figure 6:

1. First we show that the problemcan be reduced efficiently to the satisfiability problem of K# with the formulas represented as trees (and not arbitrary DAGs). Let us call this problemK# tree -sat. This will be Lemma 1.

1. Second, we show that K# tree -sat can be reduced efficiently to the satisfiability problem of K#,-1 with formulas represented as trees. This will be Lemma 2.
2. Third, we conclude by simply observing that K#,-1 can be seen as fragment of Extended Modal Logic (EML) introduced by Demri and Lugiez [2010], whose satisfiability problem is in PSPACE.

It is sufficient to establish an upper-bound on the complexity of K#, which is stated in the next proposition.

Proposition 3. The satisfiability problem of the logic K# is in PSPACE.

The initial step in both proofs of Lemma 1 and Lemma 2 shares the same idea. Given a subformula ϕ or arithmetic subexpression 1ϕ, we introduce a fresh propositional variable pϕ. The variable can then be used as a shortcut, or used in a shortcut, to refer to the truth (resp. value) of the original subformula (resp. arithmetic subexpression). An adequate formula is then added to 'factorize' the original subformula or arithmetic subexpression, and enforced at every 'relevant' world of a model to capture the intended properties of the transformations. To this end, we can rely on the modality □→mϕ, simply defined as □→mϕ := ∧0≤i≤m □iϕ, with m being the modal depth of the original formula.

To prove Proposition 3, we first show that we can efficiently transform a K# formula (represented as a DAG) into an equi-satisfiable K# formula which is represented as a tree.

For every node of the DAG that is a formula, we introduce a fresh proposition. Starting from the leafs of the DAG, we replace every subformula ψ with its corresponding proposition pψ which will simulate the truth of ψ. As we go towards the root, we replace ψ with pψ, and we add a formula of the form □→m(pψ ↔ ψ′ ), where ψ′ is a syntactic variant of ψ, using the previously introduced fresh variables in place of the original formulas. Since the root is a formula (as opposed to an arithmetic expression), we end with a conjunction of □→m(pψ ↔ ψ′ ) formulas, and a DAG consisting of only one node with the proposition pϕ which simulates the original formula. Since we are not duplicating arbitrary formulas, but only propositional variables, this process ensures that the size of the new formula (as a string or as a tree) remains polynomial in the size of the DAG. The idea is similar to Tseitin transformation [Tseitin, 1983].

Example 10. Consider the DAG depicted on Figure 4(a). We introduce the propositional variables pp, pq, p∧, p≤, and p∨, each corresponding to a node of the DAG denoting a subformula. The formula is equi-satisfiable with the formula containing the following conjuncts: p∨, □→1 (pp ↔ p), □→1 (pq ↔ q), □→1 (p∧ ↔ pp ∧ pq), □→1 (p≥ ↔ #p∧ ≤ 1p∧ ), and □→1 (p∨ ↔ p∧ ∨ p≥). For the formula to be true, p∨ must be true, and so must be p∧ or p≥, and so on.

The previous example explains the idea of the proof in order to efficiently transform formulas represented as arbitrary DAGs into equi-satisfiable formulas represented as tree. The following lemma states that result as a reduction.

Lemma 1. The satisfiability problem of the logic K# reduces to K# tree -sat in poly-time.

Now, we show that 1χ expressions can be removed efficiently and in a satisfiability-preserving way. Technically, 1χ expressions are replaced by a counting modality, counting successors with a fresh proposition pχ, which artificially simulates the truth of χ.

Example 11. We consider the formula 1χ ≥ 1. We introduce a fresh propositional variable pχ and replace the 1χ with a counting modality #pχ. Hence, we simply rewrite the K# formula into the K#,-1 formula #pχ ≥ 1. We then add a subformula that characterizes the fact that counting pχ-worlds simulates the value of 1χ. For that, we say that if χ holds, then there must be exactly one pχ-successor and if χ does not hold then there must be no pχ-successor. At the end, the formula 1χ ≥ 1 is rewritten into the K#,-1 formula:

The previous example explains the idea of the proof in order to get rid of 1χ expressions. The following lemma states that result as a reduction.

Lemma 2. When formulas are represented as trees, the satisfiability problem of the logic K# reduces to the satisfiability problem of K#,-1 in poly-time.

The logic K#,-1 can be seen as a fragment of the logic EML introduced by Demri and Lugiez [2010], where formulas are represented as strings (which have the same size as their syntactic tree representation), and whose satisfiability problem is in PSPACE. Together with Lemma 1 and Lemma 2, this proves Proposition 3. Proposition 2 and Proposition 3 allow us to conclude.

Theorem 3. The satisfiability problem of the logic K# is PSPACE-complete.

Since coPSPACE = PSPACE, the validity and unsatisfiability problems of K# formulas are also PSPACE-complete. This will be instrumental in the next section.

6 Complexity of Reasoning about GNNs

We are now ready to wrap up algorithmic results for reasoning about GNNs.

Corollary 1. When considering GNNs, the problems P1-P4 are in PSPACE.

Proof. Let us prove it for P1. For the other problems, the principle is similar. Given A, ϕ, we can check that [[A]] = [[ϕ]], by computing the K#-formula tr(A) ↔ ϕ and then check that tr(A) ↔ ϕ is valid. In order to check for validity, we check that ¬(tr(A) ↔ ϕ) is not K#-satisfiable. This can be done in poly-space via Theorem 3.

Theorem 4. Problems P1-P4 are PSPACE-complete.

Proof. Membership comes from Corollary 1. Hardness follow directly from the PSPACE-hardness of the satisfiability/unsatisfiability/validity of a K#-formula (cf. Theorem 3). Consider Aall a GNN that accepts all graphs, and Anone a GNN that rejects all graphs. Consider the following polytime reductions:

• From validity of ϕ to P1: [[Aall]] = [[ϕ]].
• From validity of ϕ to P2: [[Aall]] ⊆ [[ϕ]].
• From unsatisfiability of ϕ to P3: [[ϕ]] ⊆ [[Anone]].
• From satisfiability of ϕ to P4: [[ϕ]] ∩ [[Aall]] ̸= ∅.

7 RelatedWork

The links between graded modal logic [Fattorosi-Barnaba and Caro, 1985] and GNNs have already been observed in the literature [Barceló et al., 2020; Grohe, 2021]. We know from Barceló et al. [2020] that a GNN expressible in firstorder logic (FO) is also captured by a formula in graded modal logic. Nonetheless, graded modal logic has significant limitations as it cannot represent fundamental arithmetic properties essential to GNN computations, especially those that are not expressible in first-order logic (FO). In a similar vein of finding logical counterparts of GNNs, Cucala et al. [2023] identify a class of GNNs that corresponds to Datalog. Many works combine modal/description logic and quantitative aspects: counting (see, [Areces et al., 2010; Demri and Lugiez, 2010; Hampson, 2016; Baader et al., 2020]), or probabilities [Shirazi and Amir, 2007]. Galliani et al. [2023] extend the basic description logic ALC with a new operator to define concepts by listing features with associated weights and by specifying a threshold. They prove that reasoning wrt to a knowledge-base is EXPTIMEcomplete. Linear programming and modal logic have already been combined to solve the satisfiability problem of graded/probabilistic modal logic [Snell et al., 2012]. Our logic K#,-1 can be seen as a 'recursification' of the logic used in Sälzer and Lange [2022]. They allow for counting successors satisfying a given feature, and not any subformula. Interestingly, they allow for counting also among all vertices 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 labeled graphs, but not to give a back and forth comparison with the GNN machinery itself.

There are different ways to address explanation and verification of GNNs. One approach is to use GNNs, which are explainable by design as considered by Müller et al. [2022]. This is of course a deep debate: using models easy to use for learning, versus interpretable models [Rudin, 2019]. The choice depends on the target application. Yuan et al. [2023] provide a survey on methods used to provide explanations for GNNs by using black-box techniques. Instance-level explanations explain why a graph has been recognized by an GNN; model-level ones how a given GNN works. There are also methods based on Logic Explained Networks and variants to generate logical explanation candidates ϕ [Azzolin et al., 2022]. Once a candidate is generated we could imagine to use our problem P1 (given in the introduction) to check whether [[A]] = [[ϕ]], and thus being able to fully synthesize a trustworthy explanation. The logic K# and the results presented in this paper are thus precious tools to assist in the search of model-level explanations of GNNs.

8 Conclusion and Outlook

We presented logic K#, capturing a broad and natural class of GNNs. Furthermore, we proved that the satisfiability problem of K# is PSPACE-complete, leading to direct practical perspectives to solve formal verification and explanation problems regarding this class of GNNs.

There are several directions to go from here. First, we aim to consider a larger class of GNNs. This will require to augment the expressivity of the logic, for instance by adding other activation functions like ReLU in an extension of K#. Fortunately, SMT solvers have been extended to capture ReLU (for example see Katz et al. [2017]), but it is open how a well-defined extension of our logic looks like. Similarly, it would be useful to allow for more flexibility in the combination or aggregation functions of the considered GNNs. For example, allowing for arbitrary feedforward neural networks in the combination functions or considering the mean function as aggregation. Another idea is to allow for global readouts in the considered GNNs. A GNN with global readout does not only rely on local messages passing from neighbors to neighbors, and can instead consider the whole graph. Presumably, an extension of K# would need something akin to a universal modality to captures such behaviour.

A second interesting 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. [Blackburn et al., 2001]. 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).

A third direction of research would be to build a tool for solving verification and explainability issues of GNNs using K# as described in Section 1. The satisfiability problem of K# is in PSPACE. Many practical problems are in PSPACE (model checking against a linear temporal logic property just to cite one [Sistla and Clarke, 1985]). This means that we may rely on heuristics to guide the search, but this needs thorough investigations.

Ethical Statement

There are no ethical issues.

Acknowledgments

This work was supported by the ANR EpiRL project ANR22-CE23-0029, and by the MUR (Italy) Department of Excellence 2023-2027. We would like to thank Stéphane Demri for discussions.