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 a broad class of GNNs can be transformed efficiently into a formula, thus significantly improving upon the literature about the logical expressiveness of GNNs. We also show that the satisfiability problem is PSPACE-complete. These results bring together the promise of using standard logical methods for reasoning about GNNs and their properties, particularly in applications such as GNN querying, equivalence checking, etc. We prove that such natural problems can be solved in polynomial space.

翻译：我们提出了一种模态逻辑，其中计数模态以线性不等式的形式出现。我们证明每个公式都可以转化为等价的图神经网络（GNN）。我们还证明一大类GNN可以高效地转化为公式，从而显著改进了关于GNN逻辑表达能力的现有文献。我们进一步证明了可满足性问题是PSPACE完全的。这些结果为实现使用标准逻辑方法推理GNN及其特性带来了希望，特别是在GNN查询、等价性检查等应用中。我们证明了此类自然问题可以在多项式空间内求解。