Deciding two-variable logic with global and local Presburger quantification
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.
Related
- The good commutator approach to global asymptotics for the Schrödinger equation with variable coefficients
- Conditional Mean Independence, Global Sensitivity Analysis, and Variable Screening Using nearest neighbor Graphs
- Global Parameter Identification and Uncertainty Quantification of reduced-order ADM1 using Maximum Likelihood Estimation and Bayesian Inference
- Deciding strong quasipositivity and quasipositivity
- On deciding transcendence of power series
BibTeX
@misc{benedikt2026deciding,
title = {{Deciding two-variable logic with global and local Presburger quantification}},
author = {Michael Benedikt and Chia-Hsuan Lu and Alex Perry and Tony Tan},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2610.39108},
eprint = {2610.39108},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2610.39108},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - Deciding two-variable logic with global and local Presburger quantification
AU - Michael Benedikt
AU - Chia-Hsuan Lu
AU - Alex Perry
AU - Tony Tan
PY - 2026
DA - 2026/10/29
PB - arXiv
DO - 10.48550/arxiv.2610.39108
UR - https://arxiv.org/abs/2610.39108
AB - 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.
ER -