发表机构
Universidad Simón Bolívar（西蒙·玻利瓦尔大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本研究提出循环图神经网络与模态μ-演算片段BΣ°₁之间的双向等价，通过基于集合的聚合和可从权重检查的条件，实现无需计数逻辑或外部信号的符号解释路径。
AI 中文摘要
循环图神经网络迭代消息传递直至收敛，其至今的逻辑刻画依赖于多重集聚合、分级（计数）逻辑以及无法从网络参数中验证的停机或接受条件。我们研究采用基于集合的聚合的循环图神经网络，并识别出可从权重检查的充分条件，使得网络能够编译为公式，公式也能编译为网络。主要结果是在一类网络与可达性和安全性属性的布尔闭包（模态μ-演算的片段BΣ°₁）之间建立了有效的双向等价性。该片段并非人为构造：它正是有限词汇上稳定性的精确表达能力，支持单一极性的不动点及其布尔组合，但不支持相反极性不动点的复合。该对应关系不需要计数逻辑、外部停机信号或非有效的接受条件，从而为满足条件的网络提供了一条从权重到符号解释的可验证路径。
英文摘要
Recurrent GNNs iterate message passing to convergence, and their logical characterizations to date rely on multi-set aggregation, graded (counting) logics, and halting or acceptance conditions that cannot be verified from the network's parameters. We study recurrent GNNs with set-based aggregation and identify sufficient conditions checkable from the weights for networks to compile into formulas and formulas into networks. The main result is an effective, two-directional equivalence between a class of networks and the Boolean closure of reachability and safety properties, the fragment B$Σ^{\circ}_1$ of the modal $μ$-calculus. The fragment is not an artifact: it is the exact expressive level of stabilization over finite vocabulary, which supports fixed points of a single polarity and Boolean combinations thereof, but not the composition of fixed points of opposite polarities. The correspondence needs no counting logic, no external halting signal, and no non-effective acceptance condition, yielding a verifiable path from weights to symbolic explanations for networks meeting the conditions.
