Analysis of logics with arithmetic
Michael Benedikt, Chia-Hsuan Lu, Tony Tan
TL;DR
This work advances the theory of finite satisfiability for arithmetic-augmented two-variable logics by establishing an $\mathsf{EXP}$ upper bound for $\mathsf{GP^2}$ and providing a semilinear spectral framework for $\mathsf{C^2}$ with counting and global cardinality constraints. It introduces a Kleene-star based reduction and automata-based representations to reduce model existence to solving linear systems, enabling effective decidability analyses and modular extensions, including modulus constraints. The results clarify the relative expressive power of $\mathsf{GP^2}$ and $\mathsf{C^2}$ with global constraints and provide practical tools for analyzing logics relevant to static analysis and Graph Neural Network verification. The techniques yield concrete decision procedures and pave the way for richer arithmetic-augmented logics in finite models.
Abstract
We present new results on finite satisfiability of logics with counting and arithmetic. One result is a tight bound on the complexity of satisfiability of logics with so-called local Presburger quantifiers, which sum over neighbors of a node in a graph. A second contribution concerns computing a semilinear representation of the cardinalities associated with a formula in two variable logic extended with counting quantifiers. Such a representation allows you to get bounds not only on satisfiability for these logics, but for satisfiability in the presence of additional ``global cardinality constraints'': restrictions on cardinalities of unary formulas, expressed using arbitrary decidability logics over arithmetic. In the process, we provide simpler proofs of some key prior results on finite satisfiability and semi-linearity of the spectrum for these logics.