Deciding logic with separate local and global counting over graphs
Deciding two-variable logic with global and local Presburger quantification
Logic in Computer Science
Summary
The authors study a special kind of logic used to describe properties of networks, where you can count things both around a specific node (local) and across the entire network (global). Past work showed that mixing these two kinds of counting too freely makes it impossible to always decide if a statement is true or not. This paper proves that if you keep local and global counting separate in the logical formulas, then you can still decide their truth. This result also helps understand some kinds of graph neural networks, showing when certain analysis questions about them can be answered.
What this means in practice
- •For graph neural network engineers: Determine whether properties or equivalences of GNN models with separated local and global aggregations can be algorithmically checked.
- •For formal verification teams: Use decidability results to verify correctness and equivalence of systems modeled by graphs with separate local/global counting restrictions.
A theory result. No direct application yet.
Authors
Michael Benedikt, Chia-Hsuan Lu, Alex Perry, Tony Tan
Abstract
We look at a two-variable logic over finite graphs that allows Presburger quantifiers: linear arithmetic inequalities between the number of elements that satisfy subformulas. The prior literature shows that closing two-variable logic under Presburger quantification leads to undecidability, while closing under \emph{local quantification} -- the counts are always over neighbors of a given node -- preserves decidability. Here we show decidability of satisfiability for an intermediate logic that allows both local counts and global counts, but where the linear constraints do not mix the two. The proof requires a significant extension of the prior machinery developed for two-variable logic with counting. As a corollary we obtain decidability of satisfiability for an important family of Graph Neural Networks (GNNs). GNNs are a popular graph learning formalism. For example, in a variation of GNNs considered in the past literature, local aggregation is used in each layer to create modified values at each vertex of a graph, and then global aggregation is used in a final layer to obtain a single numerical value for the graph as a whole. Our logic is motivated by the fact that mixing of local counting and global aggregation in GNNs has been shown to lead to undecidability. Our results here show that if global and local aggregation are separated, one regains decidability. Decidability of other static analysis problems, like equivalence of GNNs, follows from the decidability of satisfiability.