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查询、等价性检验等应用中。我们证明这些自然问题可以在多项式空间内求解。