#  KW 17-002
DESY 17-186
DO-TH 17/29
Scalar one-loop vertex integrals as meromorphic functions of space-time
dimension d ††thanks: Presented at workshop “Matter To The Deepest”, XLI
International Conference on Recent Developments in Physics of Fundamental
Interactions (MTTD 2017), September 3-8, 2017, Podlesice, Poland,
http://indico.if.us.edu.pl/event/4/overview, to appear in the proceedings

Johannes Blümlein
Khiem Hong Phan
Tord Riemann SpeakerE-mail<EMAIL_ADDRESS>Deutsches Elektronen-
Synchrotron DESY, Platanenallee 6, 15738 Zeuthen, Germany  Deutsches
Elektronen-Synchrotron DESY, Platanenallee 6, 15738 Zeuthen, Germany
and
University of Science, Vietnam National University, 227 Nguyen Van Cu, Dist.5,
Ho Chi Minh City, Vietnam  Institute of Physics, University of Silesia, ul. 75
Pułku Piechoty 1, 41-500 Chorzów
and
Deutsches Elektronen-Synchrotron, DESY, Platanenallee 6, 15738 Zeuthen,
Germany

###### Abstract

Representations are derived for the basic scalar one-loop vertex Feynman
integrals as meromorphic functions of the space-time dimension $d$ in terms of
(generalized) hypergeometric functions ${}_{2}F_{1}$ and $F_{1}$. Values at
asymptotic or exceptional kinematic points as well as expansions around the
singular points at $d=4+2n$, $n$ non-negative integers, may be derived from
the representations easily. The Feynman integrals studied here may be used as
building blocks for the calculation of one-loop and higher-loop scalar and
tensor amplitudes. From the recursion relation presented, higher $n$-point
functions may be obtained in a straightforward manner.

11.80.Cr, 12.38.Bx

##  1 Introduction

The systematic treatment of Feynman integrals is one of the basic ingredients
of any perturbative calculation in quantum field theory. In gauge field
theories, the Feynman integrals may have both ultraviolet and infrared
singularities, and the necessary regularizations are usually performed using a
space-time dimension $d=4-2\epsilon$, where $\epsilon$ is the regulator. At
one loop, one has to treat two issues concerning dimensionally regularized
Feynman integrals: (i) the calculation of $n$-point integrals; (ii) the
calculation of tensor integrals. In a variety of publications it has been
shown that, besides a direct calculation, a general $n$-point tensor Feynman
integral may be algebraically reduced to a basis of scalar one- to four-point
functions [1], with higher powers $\nu$ of propagators and in higher
dimensions $d=4+2n-2\epsilon$. Using recurrence relations [2, 3, 4, 5], one
may get representations with all $\nu=1$, although yet at $d=4+2n-2\epsilon$
with non-negative integer $n$ . Such a representation in higher space-time
dimensions may be organized such that it avoids the creation of inverse Gram
determinants, which are known to destabilize realistic loop calculations [6,
7].

Having all this in mind it is evident that the seminal articles by ’t Hooft
and Veltman on scalar one-loop integrals [8] and by Passarino and Veltman on
tensor reduction [9] for one- to four point functions in 1978 set the stage
for decades. They solved the determination of the Laurent-expansions in
$\epsilon$ for these functions from the leading singular terms upto including
the constant terms, at $n=0$. Later, the leading $\epsilon$-terms were
determined in [10], and the general expansion in $\epsilon$ was studied in
[11], again at $n=0$.

Although there are many attempts to determine the scalar one-loop integrals as
meromorphic functions in the space-time dimension $d$, a complete solution in
terms of special functions has not been given so far. The most important
article on the subject is [12], where solutions have been found for scalar
one- to four-point integrals in $d$ dimensions by solving iterative difference
equations for them. The solutions depend on Gauss’ hypergeometric function for
two-point functions, additionally on the Appell function $F_{1}$ (a special
case of the Kampé de Fériet function and one of the set of Horn functions) for
three-point functions, and additionally on the Lauricella-Saran function
$F_{S}$ for four-point functions. In our understanding, the study [12] is not
complete because the authors failed to determine sufficiently general
expressions for certain boundary terms which they call $b_{3}$.

In this article, we close the above-mentioned gap left in [12] by applying
another technique, starting from Feynman parameter representations for the
Feynman integrals, deriving an iterative master integral. For vertices, we
solve here the iterative two-dimensional Mellin-Barnes representation. Our
version of the boundary term $b_{3}$ allows to cover the complete physical
kinematics in the complex $d$-plane. The most interesting case of four-point
functions with a term $b_{4}$ has also been solved and will be published
elsewhere.

##  2 Definitions

The scalar one-loop $N$-point Feynman integrals are defined as

$\displaystyle J_{n}\equiv
J_{n}(d;\\{p_{i}p_{j}\\},\\{m_{i}^{2}\\})=\int\dfrac{d^{d}k}{i\pi^{d/2}}\dfrac{1}{D_{1}^{\nu_{1}}D_{2}^{\nu_{2}}\cdots
D_{n}^{\nu_{n}}},$ (1)

with inverse propagators $D_{i}=(k+q_{i})^{2}-m_{i}^{2}+i\varepsilon$. We
assume $\nu_{i}=1$ as well as momentum conservation and all momenta to be
incoming, $\sum_{i}^{n}p_{i}=0.$ The $q_{i}$ are loop momenta shifts and will
be expressed for applications by the external momenta $p_{i}$. The
$F$-function is independent of a shift of the integration variable $k$ due to
the dependence on the differences $q_{i}-q_{j}$. Further, the difference of
two neighboring momentum shifts $q_{i}$ equals to an external momentum. We use
the Feynman parameter representation for the evaluation of the Feynman
integrals (1):

$\displaystyle J_{n}$ $\displaystyle=$
$\displaystyle(-1)^{n}{\Gamma\left(n-d/2\right)}\int_{0}^{1}\prod_{j=1}^{n}dx_{j}\delta\left(1-\sum_{i=1}^{n}x_{i}\right)\frac{1}{F_{n}(x)^{n-d/2}}.$
(2)

Here, the $F$-function is the second Symanzik polynomial. It is derived from
the propagators,
$M^{2}\equiv{x_{1}D_{1}+\cdots+x_{n}D_{n}}~{}=~{}k^{2}-2Qk+J.$ Using
$\delta(1-\sum x_{i})$ under the integral in order to transform linear terms
in $x$ into bilinear ones, one obtains

$\displaystyle F_{n}(x)$ $\displaystyle=$
$\displaystyle-\left(\sum_{i=1}^{n}x_{i}\right)\times
J+Q^{2}~{}=~{}\frac{1}{2}\sum_{i,j}x_{i}Y_{ij}x_{j}-i\varepsilon,$ (3)

where the $Y_{ij}$ are elements of the Cayley matrix, introduced for a
systematic study of one-loop $n$-point Feynman integrals e.g. in [13]:

$\displaystyle Y_{ij}=Y_{ji}$ $\displaystyle=$ $\displaystyle
m_{i}^{2}+m_{j}^{2}-(q_{i}-q_{j})^{2}.$ (4)

We will discuss the one-loop integrals as functions of two kinematic matrices
and determinants, which were introduced by Melrose [13]. The Cayley
determinant $\lambda_{12\dots n}$ is composed of the $Y_{ij}$ introduced in
(4), and its determinant is:

$\displaystyle\lambda_{n}\equiv\lambda_{12\dots n}$ $\displaystyle=$
$\displaystyle\left|\begin{array}[]{cccc}Y_{11}&Y_{12}&\ldots&Y_{1n}\\\
Y_{12}&Y_{22}&\ldots&Y_{2n}\\\ \vdots&\vdots&\ddots&\vdots\\\
Y_{1n}&Y_{2n}&\ldots&Y_{nn}\end{array}\right|.$ (9)

We also define the $(n-1)\times(n-1)$ dimensional Gram determinant,

$\displaystyle G_{n}\equiv G_{12\cdots
n}=-\left|\begin{array}[]{cccc}\\!(q_{1}-q_{n})^{2}&\ldots&(q_{1}-q_{n})(q_{n-1}-q_{n})\\\
\\!(q_{1}-q_{n})(q_{2}-q_{n})&\ldots&(q_{2}-q_{n})(q_{n-1}-q_{n})\\\
\vdots&\ddots&\vdots\\\
\\!(q_{1}-q_{n})(q_{n-1}-q_{n})&\ldots&(q_{n-1}-q_{n})^{2}\end{array}\right|.$
(14)

Both determinants are independent of a common shifting of the momenta $q_{i}$.
After elimination of one $x$-variable from the $n$-dimensional integral (1),
e.g. $x_{n}$, by use of the $\delta$-function in (2), the $F$-function becomes
a quadratic form in $x=(x_{i})$ with linear terms in $x$ and with an
inhomogeneity $R_{n}$:

$\displaystyle
F_{n}(x)=(x-y)^{T}G_{n}(x-y)+r_{n}{~{}-i\varepsilon}=\Lambda_{n}(x)+R_{n}.$
(15)

The following relations are also valid:

$\displaystyle R_{n}\equiv
r_{n}-i\varepsilon=-~{}\frac{\lambda_{n}}{G_{n}}-i\varepsilon$ (16)

and

$\displaystyle y_{i}$ $\displaystyle=$ $\displaystyle\dfrac{\partial
r_{n}}{\partial
m_{i}^{2}}~{}=~{}-\frac{1}{G_{n}}~{}\dfrac{\partial\lambda_{n}}{\partial
m_{i}^{2}}~{}\equiv~{}-\dfrac{\partial_{i}\lambda_{n}}{g_{n}},~{}~{}~{}i=1\cdots
n.$ (17)

The auxiliary condition $\sum_{i}^{n}y_{i}=1$ is fulfilled. The notations for
the $F$-function are finally independent of the choice of the variable which
was eliminated by use of the $\delta$-function in the integrand of (2). The
inhomogeneity $R_{n}$ is the only variable carrying the causal
$i\varepsilon$-prescription, while e.g. $\Lambda(x)$ and the $y_{i}$ are by
definition real.

The simplest case of a one-loop scalar Feynman integral is the one-point
function or tadpole,

$\displaystyle J_{1}(d;m^{2})$ $\displaystyle=$
$\displaystyle\int\dfrac{d^{d}k}{i\pi^{d/2}}\dfrac{1}{k^{2}-m^{2}+i\varepsilon}~{}~{}=~{}~{}-\frac{\Gamma(1-d/2)}{(m^{2}-i\varepsilon)^{1-d/2}}.$
(18)

Finally, we introduce the operator ${\bf k^{-}}$, which will reduce an
$n$-point Feynman integral $J_{n}$ to an $(n-1)$-point integral $J_{n-1}$ by
shrinking the $k^{th}$ propagator, $1/D_{k}$:

$\displaystyle{\bf k^{-}}~{}J_{n}$ $\displaystyle=$ $\displaystyle{\bf
k^{-}}\int\dfrac{d^{d}k}{i\pi^{d/2}}\dfrac{1}{\prod_{j=1}^{n}D_{j}}~{}~{}=~{}~{}\int\dfrac{d^{d}k}{i\pi^{d/2}}\dfrac{1}{\prod_{j\neq
k,j=1}^{n}D_{j}}.$ (19)

##  3 The master formula for the Feynman integrals $J_{n}$

We study the general case with $G_{n}\neq 0$ and $R_{n}\neq 0$. Other cases
are simply derived from the formulae given here. One may use the well-known
Mellin-Barnes representation in order to decompose the integrand of $J_{n}$
given in (2) as follows:

$\displaystyle\dfrac{1}{[\Lambda_{n}(x)+R_{n}]^{n-\frac{d}{2}}}=\dfrac{R_{n}^{-(n-\frac{d}{2})}}{2\pi
i}\int\limits_{-i\infty}^{+i\infty}ds\;\dfrac{\Gamma(-s)\;\Gamma(n-\frac{d}{2}+s)}{\Gamma(n-\frac{d}{2})}\left[\dfrac{\Lambda_{n}(x)}{R_{n}}\right]^{s},$
(20)

for $|\mathrm{Arg}(\Lambda_{n}/R_{n})|<\pi$. The condition always applies. As
a result of (20), the Feynman parameter integral of $J_{n}$ becomes
homogeneous:

$\displaystyle
K_{n}=\prod_{j=1}^{n-1}\int_{0}^{1-\sum_{i=j+1}^{n-1}x_{i}}dx_{j}\;\left[\dfrac{\Lambda_{n}(x)}{R_{n}}\right]^{s}~{}\equiv~{}\int
dS_{n-1}\;\left[\dfrac{\Lambda_{n}(x)}{R_{n}}\right]^{s}.$ (21)

In order to solve this integral, we introduce the differential operator
$\hat{P}_{n}$ [14, 15],

$\displaystyle\frac{\hat{P}_{n}}{s}\left[\dfrac{\Lambda_{n}(x)}{R_{n}}\right]^{s}~{}\equiv~{}\sum_{i=1}^{n-1}\frac{1}{2s}(x_{i}-y_{i})\frac{\partial}{\partial
x_{i}}\left[\dfrac{\Lambda_{n}(x)}{R_{n}}\right]^{s}=\;\left[\dfrac{\Lambda_{n}(x)}{R_{n}}\right]^{s},$
(22)

into the integrand of (21):

$\displaystyle K_{n}$ $\displaystyle=$ $\displaystyle\frac{1}{s}\int
dS_{n-1}\;\hat{P}_{n}\left[\dfrac{\Lambda_{n}(x)}{R_{n}}\right]^{s}~{}=~{}\frac{1}{2s}\sum_{i=1}^{n-1}\prod_{k=1}^{n-1}\int\limits_{0}^{u_{k}}dx^{\prime}_{k}~{}(x_{i}-y_{i})\frac{\partial}{\partial
x_{i}}\left[\dfrac{\Lambda_{n}(x)}{R_{n}}\right]^{s}.$

After a series of manipulations in order to perform one of the
$x$-integrations – by partial integration, eating the corresponding
differential –, and applying a Barnes relation [16] (item 14.53 at page 290 of
[17]), one arrives at the following recursion relation:

$\displaystyle J_{n}(d,\\{q_{i},m_{i}^{2}\\})$ $\displaystyle=$
$\displaystyle\dfrac{{-1}}{2\pi
i}\int\limits_{-i\infty}^{+i\infty}ds\dfrac{\Gamma(-s)\Gamma(\frac{d-n+1}{2}+s)\Gamma(s+1)}{2\Gamma(\frac{d-n+1}{2})}\left(\frac{1}{{R_{n}}}\right)^{s}$
(23) $\displaystyle\hskip
11.38092pt\times\sum\limits_{k=1}^{n}\left(\frac{1}{{R_{n}}}\frac{\partial{r_{n}}}{\partial
m_{k}^{2}}\right)\;{\bf k}^{-}J_{n}(d+2s;\\{q_{i},m_{i}^{2}\\}).$

Eq. (23) is the master integral for one-loop $n$-point functions in space-time
dimension $d$, representing them by $n$ integrals over $(n-1)$-point functions
with a shifted dimension $d+2s$. This Mellin-Barnes integral representation is
the equivalent to Eq. (19) of [12]. There, an infinite sum over a discrete
parameter $s$ was derived in order to represent an $n$-point function in
space-time dimension $d$ by simpler functions $J_{n-1}$ at dimensions $d+2s$.

##  4 The three-point function

According to the master formula (23), we can write the massive 3-point
function as a sum of three terms, each of them relying on a two-point
function, relying on one-point functions. After analytically performing the
two-fold Mellin-Barnes integrals, we arrive at:

$\displaystyle J_{3}(d;\\{p_{i}^{2}\\},\\{m_{i}^{2}\\})$ $\displaystyle=$
$\displaystyle J_{123}+J_{231}+J_{312},$ (24)

with

$\displaystyle J_{123}$ $\displaystyle=$
$\displaystyle\Gamma\left(2-\frac{d}{2}\right)~{}R_{3}^{\frac{d}{2}-2}~{}b_{123}$
$\displaystyle-~{}~{}\dfrac{\sqrt{\pi}~{}\Gamma\left(2-\frac{d}{2}\right)\Gamma\left(\frac{d}{2}-1\right)}{\Gamma\left(\frac{d-1}{2}\right)}~{}~{}\dfrac{\partial_{3}\lambda_{3}}{\lambda_{3}}~{}~{}\dfrac{R_{12}^{\frac{d}{2}-1}}{4\lambda_{12}}\left[\dfrac{\partial_{2}\lambda_{12}}{\sqrt{1-\frac{m_{1}^{2}}{R_{12}}}}+\dfrac{\partial_{1}\lambda_{12}}{\sqrt{1-\frac{m_{2}^{2}}{R_{12}}}}\right]$
$\displaystyle\times~{}\,{}_{2}F_{1}\\!\\!\left[\begin{array}[]{c}\frac{d-2}{2},1\,;\\\
\frac{d-1}{2}\,;\end{array}\dfrac{R_{12}}{R_{3}}\right]~{}{+}~{}\frac{2}{d-2}\Gamma\left(2-\frac{d}{2}\right)~{}\dfrac{\partial_{3}\lambda_{3}}{\lambda_{3}}$
$\displaystyle\hskip
28.45274pt\times\left[\dfrac{\partial_{2}\lambda_{12}}{\sqrt{1-\frac{m_{1}^{2}}{R_{12}}}}\dfrac{(m_{1}^{2})^{\frac{d}{2}-1}}{4\lambda_{12}}F_{1}\left(\dfrac{d-2}{2};1,\frac{1}{2};\frac{d}{2};\frac{m_{1}^{2}}{R_{3}},\dfrac{m_{1}^{2}}{R_{12}}\right)+(1\leftrightarrow
2)\right],$

and

$\displaystyle b_{123}$ $\displaystyle=$
$\displaystyle-\frac{1}{2G_{12}}~{}\dfrac{\partial_{3}\lambda_{3}}{\lambda_{3}}~{}\left(\dfrac{\partial_{2}\lambda_{12}}{\sqrt{1-\frac{m_{1}^{2}}{R_{12}}}}+\dfrac{\partial_{1}\lambda_{12}}{\sqrt{1-\frac{m_{2}^{2}}{R_{12}}}}\right)\,{}_{2}F_{1}\\!\\!\left[\begin{array}[]{c}1,1\,;\\\
\frac{3}{2}\,;\end{array}\dfrac{R_{12}}{R_{3}}\right]$
$\displaystyle-\dfrac{\partial_{3}\lambda_{3}}{\lambda_{3}}\left\\{\dfrac{\partial_{2}\lambda_{12}}{\sqrt{1-\frac{m_{1}^{2}}{R_{12}}}}\;\dfrac{m_{1}^{2}}{4\lambda_{12}}\;F_{1}\left(1;1,\frac{1}{2};2;\frac{m_{1}^{2}}{R_{3}},\dfrac{m_{1}^{2}}{R_{12}}\right)+(1\leftrightarrow
2)\right\\},$

where $\partial_{i}\lambda_{j\cdots}$ is defined in (17). The representation
(24) is valid for Re$\Big{(}\frac{d-2}{2}\Big{)}>0$. The conditions
$\Big{|}\frac{m_{i}^{2}}{R_{ij}}\Big{|}<1$,
$\Big{|}\frac{R_{ij}}{R_{3}}\Big{|}<1$ had to be met during the derivation.
The result may be analytically continued in a straightforward way, however, in
the complete complex domain.

##  5 Vertex numerics

In Table 1 we show one numerical case, further examples are given in the
slides of the presentation at MTTD 2018, see
http://indico.if.us.edu.pl/event/4/. While we agree completely with the “main”
parts of the solutions for the Feynman integrals given in [12], our boundary
term has a richer structure and is, contrary to $b_{3}$ [12], valid for
arbitrary kinematics without additional specific considerations.

[$p_{i}^{2}$], [$m_{i}^{2}$] | [-100, +200, -300], [10, 20, 30]
---|---
$G_{3}$, $\lambda_{3}$ |  +480000, –19300000
$m_{i}^{2}/r_{3}$ | 0.248705, 0.497409, 0.746114
$\sum J$, eq. (4) | –0.012307377 – 0.056679689 I
$\sum b$, eq. (4) | \+ 0.047378343 I
$J_{3}^{(TR)}$ $=\sum J+\sum b$ | –0.012307377 – 0.009301346 I
$b_{3}$ [12] | \+ 0.047378343 I
$b_{3}$+$\sum J~{}\cite[cite]{[\@@bibref{}{Fleischer:2003rm}{}{}]}$ | –0.012307377 – 0.009301346 I
$J_{3}^{(OT)}=\sum J$ |  $b_{3}\to 0$, gets wrong
(-1)$\times$FIESTA 3 [18] | –(0.012307 + 0.009301 I)
LoopTools/FF [19] | –0.012307377 – 0.009301346 I
Table 1:  Numerics for the constant term of a vertex in space-time dimension
$d=4-2\epsilon$. Causal $\varepsilon=10^{-20}$. This work, (24) to (4) is
labelled (TR). Bold input quantities suggest that, according to eq. (73) in
[12] (labelled (OT)), one has to set there $b_{3}=0$. This choice gives a
wrong result for $J_{3}$. If instead we choose in the numerics for eq. (75) of
[12] that $\sqrt{-G_{3}}\to\sqrt{-G_{3}+\varepsilon I}=+I\sqrt{|G_{3}|}$, and
include the non-vanishing value for $b_{3}$, the $J_{3}^{(OT)}$ gets correct.
The setting $G_{3}-\varepsilon I$ looks counter-intuitive for a
“momentum”-like function like $G_{3}$.

## Acknowledgements

This work was supported in part by the European Commission through contract
PITN-GA-2012-316704 (HIGGSTOOLS). K.H.P. would like to thank DESY for
hospitality and support during the present project. His work is also supported
by the Vietnam National Foundation for Science and Technology Development
(NAFOSTED) under the grant No 103.01-2016.33. The work of T.R. is supported in
part by the Polish Alexander von Humboldt Honorary Research Fellowship 2015.
We thank Ievgen Dubovyk and Johann Usovitsch for assistance in several
numerical comparisons with the MB-suite AMBRE/MB/mbtools/MBnumerics/CUBA [20,
21, 22, 23, 24, 25, 26].

## References

  * [1] A. I. Davydychev, A Simple formula for reducing Feynman diagrams to scalar integrals, Phys. Lett. B263 (1991) 107–111, http://wwwthep.physik.uni-mainz.de/~davyd/preprints/tensor1.pdf.  doi:10.1016/0370-2693(91)91715-8.
  * [2] K. Chetyrkin, F. Tkachov, Integration by parts: The algorithm to calculate $\beta$ functions in 4 loops, Nucl.Phys. B192 (1981) 159–204.  doi:10.1016/0550-3213(81)90199-1.
  * [3] F. V. Tkachov, A theorem on analytical calculability of four loop renormalization group functions, Phys. Lett. 100B (1981) 65–68.  doi:10.1016/0370-2693(81)90288-4.
  * [4] O. Tarasov, Connection between Feynman integrals having different values of the space-time dimension, Phys. Rev. D54 (1996) 6479–6490.  arXiv:hep-th/9606018, doi:10.1103/PhysRevD.54.6479.
  * [5] J. Fleischer, F. Jegerlehner, O. Tarasov, Algebraic reduction of one loop Feynman graph amplitudes, Nucl. Phys. B566 (2000) 423.  arXiv:hep-ph/9907327, doi:10.1016/S0550-3213(99)00678-1.
  * [6] J. Fleischer, T. Riemann, A complete algebraic reduction of one-loop tensor Feynman integrals, Phys. Rev. D83 (2011) 073004.  arXiv:1009.4436, doi:10.1103/PhysRevD.83.073004.
  * [7] T. Riemann, A. Almasy, J. Gluza and I. Dubovyk, Contraction of 1-loop 5-point tensor Feynman integrals, talk held at ACAT 2013, May 2013, Beijing, China. http://indico.ihep.ac.cn/event/2813/session/6/contribution/4/material/slides/0.pdf.
  * [8] G. ’t Hooft, M. Veltman, Scalar One Loop Integrals, Nucl. Phys. B153 (1979) 365–401, available from the Utrecht University Repository as https://dspace.library.uu.nl/bitstream/handle/1874/4847/14006.pdf?sequence=2&isAllowed=y.  doi:10.1016/0550-3213(79)90605-9.
  * [9] G. Passarino, M. Veltman, One loop corrections for $e^{+}e^{-}$ annihilation into $\mu^{+}\mu^{-}$ in the Weinberg model, Nucl. Phys. B160 (1979) 151.  doi:10.1016/0550-3213(79)90234-7.
  * [10] U. Nierste, D. Müller, M. Böhm, Two loop relevant parts of D-dimensional massive scalar one loop integrals, Z. Phys. C57 (1993) 605–614.  doi:10.1007/BF01561479.
  * [11] G. Passarino, An approach toward the numerical evaluation of multiloop Feynman diagrams, Nucl. Phys. B619 (2001) 257–312.  arXiv:hep-ph/0108252, doi:10.1016/S0550-3213(01)00528-4.
  * [12] J. Fleischer, F. Jegerlehner, O. Tarasov, A new hypergeometric representation of one loop scalar integrals in d dimensions, Nucl. Phys. B672 (2003) 303.  arXiv:hep-ph/0307113, doi:10.1016/j.nuclphysb.2003.09.004.
  * [13] D. B. Melrose, Reduction of Feynman diagrams, Nuovo Cim. 40 (1965) 181–213, available from http://www.physics.usyd.edu.au/theory/melrose_publications/PDF60s/1965.pdf.  doi:10.1007/BF028329.
  * [14] I. Bernshtein, Modules over a ring of differential operators.Moscow State University, translated from Funktsional’nyi Analiz i Ego Prilozheniya, Vol. 5, pp. 1-16, April 1971. Available at http://www.math1.tau.ac.il/~bernstei/Publication_list/publication_texts/bernstein-mod-dif-FAN.pdf.  doi:10.1007/BF01076413.
  * [15] V.A. Golubeva and V.Z. $\acute{\text{E}}$nol’skii, The differential equations for the Feynman amplitude of a single-loop graph with four vertices, Mathematical Notes of the Academy of Sciences of the USSR 23 (1978) 63.  doi:10.1007/BF01104888, available at http://www.mathnet.ru/links/c4b9d8a15c8714d3d8478d1d7b17609b/mzm8124.pdf.
  * [16] E. W. Barnes, A new development of the theory of the hypergeometric functions, Proc. Lond. Math. Soc. (2) 6 (1908) 141–177.  doi:10.1112/plms/s2-6.1.141.
  * [17] G. N. Watson, A treatise on the theory of Bessel functions, Cambridge University Press 1922, https://www.forgottenbooks.com/de/download/ATreatiseontheTheoryofBesselFunctions_10019747.pdf.
  * [18] A. V. Smirnov, FIESTA 3: cluster-parallelizable multiloop numerical calculations in physical regions, Comput. Phys. Commun. 185 (2014) 2090–2100.  arXiv:1312.3186, doi:10.1016/j.cpc.2014.03.015.
  * [19] T. Hahn, M. Perez-Victoria, Automatized one loop calculations in four-dimensions and D-dimensions, Comput. Phys. Commun. 118 (1999) 153.  arXiv:hep-ph/9807565, doi:10.1016/S0010-4655(98)00173-8.
  * [20] J. Gluza, K. Kajda, T. Riemann, AMBRE - a Mathematica package for the construction of Mellin-Barnes representations for Feynman integrals, Comput. Phys. Commun. 177 (2007) 879.  arXiv:0704.2423, doi:10.1016/j.cpc.2007.07.001.
  * [21] J. Gluza, K. Kajda, T. Riemann, V. Yundin, Numerical Evaluation of Tensor Feynman Integrals in Euclidean Kinematics, Eur. Phys. J. C71 (2011) 1516.  arXiv:1010.1667, doi:10.1140/epjc/s10052-010-1516-y.
  * [22] I. Dubovyk, J. Gluza, T. Riemann, J. Usovitsch, Numerical integration of massive two-loop Mellin-Barnes integrals in Minkowskian regions, PoS LL2016 (2016) 34.  arXiv:1607.07538.
  * [23] M. Czakon, Automatized analytic continuation of Mellin-Barnes integrals, Comput. Phys. Commun. 175 (2006) 559–571.  arXiv:hep-ph/0511200, doi:10.1016/j.cpc.2006.07.002.
  * [24] M. Czakon (MB, MBasymptotics), D. Kosower (barnesroutines), A. Smirnov, V. Smirnov (MBresolve), K. Bielas, I. Dubovyk, J. Gluza, K. Kajda, T. Riemann (AMBRE, PlanarityTest), MBtools webpage, https://mbtools.hepforge.org/.
  * [25] J. Usovitsch, MBnumerics, a Mathematica/Fortran package for the numerical calculation of multiple MB-integral representations for Feynman integrals, in preparation.
  * [26] T. Hahn, CUBA: A library for multidimensional numerical integration, Comput. Phys. Commun. 168 (2005) 78–95.  arXiv:hep-ph/0404043, doi:10.1016/j.cpc.2005.01.010.


11institutetext: Université de Rennes

# A Modal Logic for Explaining some Graph Neural Networks

Pierre Nunn and Francois Schwarzentruber

(October 2022)

###### 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 $\Diamond musician$, 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]]=[[\varphi]]$

P2: Verification of an explanation

  * •

input: a GNN $A$, a logical formula $\varphi$

  * •

output: yes, if $[[A]]\subseteq[[\varphi]]$

P3: Verification of an explanation

  * •

input: a GNN $A$, a logical formula $\varphi$

  * •

output: yes, if $[[\varphi]]\subseteq[[A]]$

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 $\Diamond^{\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\rightarrow tr(A)$ valid?

  * •

P4: is $\varphi\land 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)\land\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},\dots,p_{k}$. The initial state $x_{0}$ is defined by:

$x_{0}(u)=(\ell(u)(p_{1}),\dots,\ell(u)(p_{k}),0,\dots,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.

$u$$x_{t-1}$$AGG$$COMB$$u$$x_{t}$ 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 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).

$x_{0}$layer 1$x_{1}$layer 2$x_{2}$CLS1101 Figure 2: General idea of a GNN
with 2 layers applied on a graph with 4 vertices.

###### 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.$

##  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.

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

$\displaystyle\varphi$
$\displaystyle::=p\mid\lnot\varphi\mid\varphi\lor\varphi\mid E\geq 0$
$\displaystyle E$ $\displaystyle::=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)\land(-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-Fraïssé game.

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

$\displaystyle sub(p)$ $\displaystyle=\\{p\\}$ $\displaystyle
sub(\lnot\varphi)$ $\displaystyle=\\{\lnot\varphi\\}\cup sub(\varphi)$
$\displaystyle sub(\varphi\lor\psi)$ $\displaystyle=\\{\varphi\lor\psi\\}\cup
sub(\varphi)\cup sub(\psi)$ $\displaystyle sub(E\geq 0)$
$\displaystyle=\\{E\geq 0\\}\cup\bigcup\\{sub(\psi)\mid\text{$1_{\psi}$ or
$\\#\psi$ 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$:

$\displaystyle md(p)$ $\displaystyle=0$ $\displaystyle md(\lnot\varphi)$
$\displaystyle=md(\varphi)$ $\displaystyle md(\varphi\lor\psi)$
$\displaystyle=\max(md(\varphi),md(\psi))$ $\displaystyle md(E\geq 0)$
$\displaystyle=md(E)$

$\displaystyle md(c)$ $\displaystyle=0$ $\displaystyle md(1_{\varphi})$
$\displaystyle=md(\varphi)$ $\displaystyle md(\\#\varphi)$
$\displaystyle=md(\varphi)+1$ $\displaystyle md(E_{1}+E_{2})$
$\displaystyle=max(md(E_{1}),md(E_{2}))$ $\displaystyle md(k*E)$
$\displaystyle=md(E)$

As in modal logic, modalities are organized in levels.

###### Example 3

$md((1_{p\land\\#{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\land q)\geq 1_{p\land q}$ is represented by the following DAG in which
$p\land q$ is used twice:

$\leq$$\\#$$1_{...}$$\land$$p$$q$

###  3.2 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.

$(G,u)\models p$ | if | $\ell(u)(p)=1$
---|---|---
$(G,u)\models\neg\varphi$ | if | it is not the case that $(G,u)\models\varphi$
$(G,u)\models\varphi\land\psi$ | if |  $(G,u)\models\varphi$ and $(G,u)\models\psi$
$(G,u)\models E\geq 0$ | if | $[[E]]_{G,u}\geq 0$

$\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

$p$$u$$q$$p$ Figure 3: Example of a pointed graph $G,u$. We indicate true
propositional variables at each vertex.

Consider the pointed graph $G,u$ shown in Figure 3. We have $G,u\models
p\land(\\#\lnot p\geq 2)\land\\#(\\#p\geq 1)\leq 1$. Indeed, $p$ holds in $u$,
$u$ has (at least) two successors in which $\lnot 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$.

###### 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.

###  4.1 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. 1.

Either the number of layers and the dimension of the states in $A$ is
$|\varphi|$;

  2. 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:

$\displaystyle AGG(X)$ $\displaystyle=\sum_{x\in X}\textbf{x}$ $\displaystyle
COMB(x,y)$ $\displaystyle=\vec{\sigma}(xC+yA+b)$

where $\vec{\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:

$\varphi_{\ell}$ |  $\ell$-th columns of $C$ and $A$ | $b_{\ell}$
---|---|---
$p$ | $C_{\ell\ell}=1$ | 0
$\lnot\varphi_{i}$ | $C_{i\ell}=-1$ | 1
$\varphi_{i}\lor\varphi_{j}$ | $C_{i\ell}=C_{j\ell}=1$ | 0
$\varphi_{i}\land\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}$ |

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:

$\varphi_{\ell}$ |  $\ell$-th column of $C$ | $b_{\ell}$
---|---|---
$\bigvee_{i\in I}\varphi^{\prime\prime}_{i}\vee\bigvee_{i\in I^{\prime}}\neg\varphi^{\prime\prime}_{i}$ | $C_{i\ell}=\begin{cases}1\text{ for $i\in I$}\\\ -1\text{for $i\in I^{\prime}$}\end{cases}$ | $card(I^{\prime})$
$\bigwedge_{i\in I}\varphi^{\prime\prime}_{i}$ |  $C_{i\ell}=1$ for $i\in I$ | $-card(I)+1$

###### 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)=\vec{\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$.

###  4.2 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}\textbf{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},\dots,p_{k},\bot,\dots,\bot)$.

Suppose that states $x_{t}(v)$ are represented by the formulas
$(\varphi_{1},\dots,\varphi_{d})$. Then if the combination function is
$COMB(x,y)=\vec{\sigma}(xC+yA+b)$ then the states $x_{t+1}(v)$ are represented
by the formulas $(\varphi^{\prime}_{1},\dots,\varphi^{\prime}_{d})$ where
$\varphi^{\prime}_{\ell}$ 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},\dots,\varphi_{d})$ to represent
$x_{L}(v)$. As $CLS$ is linear, the final formula is
$1_{CLS(1_{\varphi_{1}},\dots,1_{\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.

###  5.1 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},\dots\\#\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+\\#\lnot p=\\#q+\\#\lnot 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 $\lnot\psi_{i}$. We define for all words $w\in\\{0,1\\}^{n}$:

$conj_{w}:=\bigwedge_{i=1..n\mid w_{i}=1}\psi_{i}\land\bigwedge_{i=1..n\mid
w_{i}=0}\lnot\psi_{i}.$

###### Example 6

$conj_{0100}=\lnot\psi_{1}\land\psi_{2}\land\lnot\psi_{3}\land\lnot\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\mid w_{i}=1}x_{w}$.

###### Example 7

How do we guarantee that $\\#p+\\#\lnot p=\\#q+\\#\lnot q$? Suppose that
$\psi_{1}=p,\psi_{2}=\lnot p,\psi_{3}=q,\psi_{4}=\lnot q$. As $p\land\lnot 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\land\lnot p$ and $q\land\lnot q$ are
unsatisfiable $x_{00**}=0$, $x_{**00}=0$ and $x_{**11}=0$. Finally:

$\displaystyle\\#p=x_{1010}+x_{1001}$ $\displaystyle\\#\lnot
p=x_{0110}+x_{0101}$ $\displaystyle\\#q=x_{1010}+x_{0110}$
$\displaystyle\\#\lnot q=x_{1001}+x_{0101}$

We see that $\\#p+\\#\lnot p=x_{1010}+x_{1001}+x_{0110}+x_{0101}=\\#q+\\#\lnot
q$.

1:function sat($\varphi$)

2: for $S\leftarrow hintikkaSet(\varphi)$ do

3: $S:=$ the set of inequalities in $S$ (clean-up)

4: Let $\\#\psi_{1},\dots\\#\psi_{n}$ be the variables of the form $\\#\psi$
appearing in $S$

5: Consider LP-variables $x_{w}$ for all $w\in\\{0,1\\}^{n}$

6: Replace $\\#\psi_{i}$ by $\sum_{w\mid w_{i}=1}x_{w}$ in $S$

7: for $w\in\\{0,1\\}^{n}$ do

8: if not sat($conj_{w}$) then

9: add constraint $x_{w}=0$ to $S$

10: if the oracle says that $S$ is ILP-satisfiable then

11: return true

12: return false

Figure 4: Algorithm for checking the satisfiability of a $K^{\\#}$-formula
$\varphi$.

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. 1.

$\varphi\in\Sigma$;

  2. 2.

if $\psi_{1}\land\psi_{2}\in\Sigma$ then $\psi_{1}\in\Sigma$ and
$\psi_{2}\in\Sigma$

  3. 3.

if $\psi_{1}\lor\psi_{2}\in\Sigma$ then $\psi_{1}\in\Sigma$ or
$\psi_{2}\in\Sigma$

  4. 4.

for all $\psi$, $\psi\not\in\Sigma$ or $\lnot\psi\not\in\Sigma$

  5. 5.

$1_{\psi}$ appears in $\varphi$, either $\psi\in\Sigma$ and
$1_{\psi}=1\in\Sigma$, or $\lnot\psi\in\Sigma$ and $1_{\psi}=0\in\Sigma$.

Point 1 says that $\varphi$ should be true. In point 3, if
$\psi_{1}\lor\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\land(\\#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,\lnot 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.

###  5.2 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)$. $\Rightarrow$ 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\mid w_{i}=1}x_{w}$. So $S$ is ILP-satisfiable, and the algorithm
returns true.

$\Leftarrow$ 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, 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\mid
w_{i}=1}x_{w}$. Thus, the obtained pointed $G,u$ is a model of $\varphi$.
Figure 5 shows an example of the construction.

$\ell(u)$$u$$u_{01}$$u_{01}$$u_{11}$$u_{11}$$u_{11}$ Figure 5: Example of a
model $G,u$ with $x_{00}=0$, $x_{01}=2$, $x_{10}=0$ and $x_{11}=3$.

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.

###  5.3 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.1

The satisfiability problem of $K^{\\#}$ is decidable and is in
$\mathsf{EXPTIME}^{\mathsf{NP}}$.

###  5.4 $\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...0}$, $conj_{010...0}$, …, $conj_{0...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
$\\#\lnot\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\dots\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)$.

## References

  * [1] Carlos Areces, Guillaume Hoffmann, and Alexandre Denis.  Modal logics with counting.  In Anuj Dawar and Ruy J. G. B. de Queiroz, editors, Logic, Language, Information and Computation, 17th International Workshop, WoLLIC 2010, Brasilia, Brazil, July 6-9, 2010. Proceedings, volume 6188 of Lecture Notes in Computer Science, pages 98–109. Springer, 2010.
  * [2] Steve Azzolin, Antonio Longa, Pietro Barbiero, Pietro Liò, and Andrea Passerini.  Global explainability of gnns via logic combination of learned concepts.  CoRR, abs/2210.07147, 2022.
  * [3] Pablo Barceló, Egor V Kostylev, Mikaël Monet, Jorge Pérez, Juan Reutter, and Juan-Pablo Silva.  THE LOGICAL EXPRESSIVENESS OF GRAPH NEURAL NETWORKS.  In 8th International Conference on Learning Representations (ICLR 2020), Virtual conference, Ethiopia, April 2020.
  * [4] Patrick Blackburn, Maarten de Rijke, and Yde Venema.  Modal Logic, volume 53 of Cambridge Tracts in Theoretical Computer Science.  Cambridge University Press, 2001.
  * [5] Artur S. d’Avila Garcez, Luís C. Lamb, and Dov M. Gabbay.  Connectionist modal logic: Representing modalities in neural networks.  Theor. Comput. Sci., 371(1-2):34–53, 2007.
  * [6] Maurizio Fattorosi-Barnaba and F. Caro.  Graded modalities. I.  Stud Logica, 44(2):197–221, 1985.
  * [7] Rajeev Goré.  Tableau methods for modal and temporal logics.  Handbook of tableau methods, pages 297–396, 1999.
  * [8] Martin Grohe.  The Logic of Graph Neural Networks, January 2022.  arXiv:2104.14624 [cs].
  * [9] Christopher Hampson.  Decidable first-order modal logics with counting quantifiers.  In Lev D. Beklemishev, Stéphane Demri, and András Maté, editors, Advances in Modal Logic 11, proceedings of the 11th conference on "Advances in Modal Logic," held in Budapest, Hungary, August 30 \- September 2, 2016, pages 382–400. College Publications, 2016.
  * [10] Shuichi Hirahara.  Identifying an honest exp^np oracle among many.  In David Zuckerman, editor, 30th Conference on Computational Complexity, CCC 2015, June 17-19, 2015, Portland, Oregon, USA, volume 33 of LIPIcs, pages 244–263. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015.
  * [11] Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, and Mykel J. Kochenderfer.  Reluplex: An efficient SMT solver for verifying deep neural networks.  In Rupak Majumdar and Viktor Kuncak, editors, Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I, volume 10426 of Lecture Notes in Computer Science, pages 97–117. Springer, 2017.
  * [12] Peter Müller, Lukas Faber, Karolis Martinkus, and Roger Wattenhofer.  DT+GNN: A fully explainable graph neural network using decision trees.  CoRR, abs/2205.13234, 2022.
  * [13] Christos H. Papadimitriou.  On the complexity of integer programming.  J. ACM, 28(4):765–768, 1981.
  * [14] Sophie Pinchinat, Sasha Rubin, and François Schwarzentruber.  Formula synthesis in propositional dynamic logic with shuffle.  In Thirty-Sixth AAAI Conference on Artificial Intelligence, AAAI 2022, Thirty-Fourth Conference on Innovative Applications of Artificial Intelligence, IAAI 2022, The Twelveth Symposium on Educational Advances in Artificial Intelligence, EAAI 2022 Virtual Event, February 22 - March 1, 2022, pages 9902–9909. AAAI Press, 2022.
  * [15] Cynthia Rudin.  Stop explaining black box machine learning models for high stakes decisions and use interpretable models instead.  Nat. Mach. Intell., 1(5):206–215, 2019.
  * [16] Amirreza Salamat, Xiao Luo, and Ali Jafari.  Heterographrec: A heterogeneous graph-based neural networks for social recommendations.  Knowl. Based Syst., 217:106817, 2021.
  * [17] Marco Sälzer and Martin Lange.  We cannot guarantee safety: The undecidability of graph neural network verification.  CoRR, abs/2206.05070, 2022.
  * [18] Franco Scarselli, Marco Gori, Ah Chung Tsoi, Markus Hagenbuchner, and Gabriele Monfardini.  The Graph Neural Network Model.  IEEE Transactions on Neural Networks, 20(1):61–80, January 2009\.
  * [19] Jeremy Seligman, Fenrong Liu, and Patrick Girard.  Facebook and the epistemic logic of friendship.  In Burkhard C. Schipper, editor, Proceedings of the 14th Conference on Theoretical Aspects of Rationality and Knowledge (TARK 2013), Chennai, India, January 7-9, 2013, 2013.
  * [20] Afsaneh Shirazi and Eyal Amir.  Probabilistic modal logic.  In Proceedings of the Twenty-Second AAAI Conference on Artificial Intelligence, July 22-26, 2007, Vancouver, British Columbia, Canada, pages 489–495. AAAI Press, 2007.
  * [21] William Snell, Dirk Pattinson, and Florian Widmann.  Solving graded/probabilistic modal logic via linear inequalities (system description).  In Nikolaj S. Bjørner and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning - 18th International Conference, LPAR-18, Mérida, Venezuela, March 11-15, 2012. Proceedings, volume 7180 of Lecture Notes in Computer Science, pages 383–390. Springer, 2012.
  * [22] Dong Wang, Xiaodong Wang, and Shaohe Lv.  End-to-end mandarin speech recognition combining CNN and BLSTM.  Symmetry, 11(5):644, 2019.
  * [23] R. Ryan Williams.  Some estimated likelihoods for computational complexity.  In Bernhard Steffen and Gerhard J. Woeginger, editors, Computing and Software Science - State of the Art and Perspectives, volume 10000 of Lecture Notes in Computer Science, pages 9–26. Springer, 2019.
  * [24] Hao Yuan, Haiyang Yu, Shurui Gui, and Shuiwang Ji.  Explainability in graph neural networks: A taxonomic survey.  IEEE Trans. Pattern Anal. Mach. Intell., 45(5):5782–5799, 2023\.
  * [25] Jie Zhou, Ganqu Cui, Shengding Hu, Zhengyan Zhang, Cheng Yang, Zhiyuan Liu, Lifeng Wang, Changcheng Li, and Maosong Sun.  Graph neural networks: A review of methods and applications.  AI Open, 1:57–81, 2020.

##  Appendix 0.A Appendix

###  0.A.1 Proof that $K^{\\#}$ is more expressive than FO (Example 2)

We show that $K^{\\#}$ is more expressive than FO by proving that the formula
$\\#p\geq\\#q$ is not expressible by a FO formula $\varphi(x)$. We observe
that if the property ‘for all vertices of a graph $\\#p\geq\\#q$’ is not
expressible in FO, then the FO formula $\varphi(x)$ doesn’t exist, because if
it existed the property would be expressible in FO by the formula $\forall
x\varphi(x)$.

For each integer $n>0$, we consider the graphs $A_{n}$ and $B_{n}$ such that
every vertices of $A_{n}$ verify $\\#p\geq\\#q$ while this is not the case for
$B_{n}$ :

$p$$p$$...$$w$$u_{1}$$u_{2}$$u_{n}$$p$$q$$q$$...$$v_{1}$$v_{2}$$v_{n}$$q$$p$$p$$...$$w^{\prime}$$u^{\prime}_{1}$$u^{\prime}_{2}$$u^{\prime}_{n}$$p$$q$$q$$...$$v^{\prime}_{1}$$v^{\prime}_{2}$$v^{\prime}_{n}$$v^{\prime}_{n+1}$$q$$q$$A_{n}$$B_{n}$

An $n$-round Ehrenfeucht-Fraïssé game is a game between two players, the
spoiler and the duplicator played on two graphs $A=(V_{A},E_{A},\ell_{A})$ and
$B=(V_{B},E_{B},\ell_{B})$. We suppose that On each round the spoiler picks
one graph and a vertex in this graph. The duplicator then chooses a vertex on
the other graph. We have $n$ vertices ($a_{1}$,$a_{2}$,…,$a_{n}$) chosen in
$A$ and $n$ vertices ($b_{1}$,$b_{2}$,…,$b_{n}$) chosen in $B$. The duplicator
wins if and only if for $1\leq i,j\leq n$ :

$a_{i}=a_{j}\Leftrightarrow b_{i}=b_{j}$

$(a_{i},a_{j})\in E_{A}\Leftrightarrow(b_{i},b_{j})\in E_{B}$

$\ell(a_{i})=\ell(b_{i})$

On the graphs $A_{n}$ and $B_{n}$, the duplicator wins the Ehrenfeucht-Fraïssé
game with $n$ rounds: if the spoiler chooses $w$ (resp. $w^{\prime}$) the
duplicator chooses $w^{\prime}$ (resp. $w$), if the spoiler chooses some
$u_{i}$ or $v_{i}$ (resp. $u^{\prime}_{i}$ or $v^{\prime}_{i}$) the duplicator
chooses $u^{\prime}_{j}$ or $v^{\prime}_{j}$ (resp. $u^{\prime}_{j}$ or
$v^{\prime}_{j}$) (If the world chosen by spoiler has not be chosen in the
previous round the duplicator pick a fresh index $j$. Else the duplicator pick
the $j$ corresponding to the world chosen in the previous rounds). Since there
are only $n$ distinct values that $i$ can take , the duplicator will win the
game in $n$ rounds with her strategy. Thus the property "for every vertices of
a graph, $\\#p\geq\\#q$ is not expressible in FO. Therefore $K^{\\#}$ is more
expressive than FO.