halting 型循环图神经网络与分级 μ 微积分

图神经网络（GNNs）是一类 operate on graph-structured data 的机器学习模型，其表达能力与在 graded bisimilarity 意义下保持不变的逻辑密切相关。当前针对循环 GNNs 的方案要么假设将图大小提供给模型，要么缺乏终止保证。在本文中，我们提出一种循环 GNNs 的 halting 机制。我们证明了我们的 halting 模型能够表达即使对于无图大小信息的标准 GNNs 变体亦可表达的 graded 模态 μ 微积分中可定义的所有节点分类器。为证明我们的主要结果，我们发展了一种新的 graded μ 微积分近似语义，该语义值得独立关注。我们将这种新语义引入一种称为计数算法的新模型检查算法，该算法对图大小毫无所知。最终我们展示，计数算法可在 halting 循环 GNN 上实现。