Technical Summary: Fast Ramsey Quantifier Elimination in LIRA

Problem Statement

Program verification, particularly for infinite-state systems, often requires reasoning about properties that are not expressible in standard first-order logic. While Satisfiability Modulo Theories (SMT) solvers effectively handle safety properties using first-order theories (e.g., Linear Integer Arithmetic - LIA, Linear Real Arithmetic - LRA), proving liveness (such as termination) typically requires reasoning about well-foundedness. This property is not first-order definable, even with recursive predicates.

Recent work has proposed Ramsey quantifiers as a unified framework to handle such properties. A Ramsey quantifier, denoted $\exists^{\text{ram}} x, y: \phi(x, y, z)$, asserts the existence of an infinite directed clique in the graph defined by $\phi$. Specifically, it is true if there exists an infinite sequence of pairwise distinct vectors $a_1, a_2, \dots$ such that $\phi(a_i, a_j, z)$ holds for all $1 \le i < j$. This formalism allows encoding liveness and monadic decomposability.

However, despite theoretical proofs that Ramsey quantifiers can be eliminated in polynomial time for the existential fragments of LIA, LRA, and the mixed case (LIRA), practical implementation has been lacking. Previous implementations were:

1. Prototypical and limited: Existing tools were primarily prototypes for LIA and LRA, with no complete implementation for the mixed LIRA case.
2. Scalability issues: Testing was restricted to small micro-benchmarks.
3. Usability barriers: Implementations relied heavily on specific APIs (e.g., Z3 Python), preventing users from specifying constraints in standard SMT-LIB formats or integrating with other solvers.

Methodology

The paper presents REAL (Ramsey Elimination for Arithmetic Logic), a solver-agnostic tool designed to eliminate Ramsey quantifiers from existential formulas in LIA, LRA, and LIRA. The methodology involves a three-stage pipeline:

1. Input Specification (SMT-LIB Extension):
   REAL extends the SMT-LIB standard to support Ramsey quantifiers. It introduces new syntax rules for terms, allowing users to specify constraints using (ramsey ...) constructs. This enables the tool to accept inputs in a standardized format rather than relying on proprietary API calls.

2. Elimination Algorithm:
   Building on the theoretical framework established in prior work [5], REAL computes an equivalent formula containing only standard existential quantifiers. The algorithm:

   • Replaces existentially quantified variables in the original formula with additional Ramsey quantified variables.
   • Identifies sufficient and necessary conditions for the existence of an infinite clique, formulating them as existential LIRA formulas.
   • For example, a condition requiring an infinite sequence $a, a+b, a+2b, \dots$ is translated into constraints on the base vector $a$ and the step vector $b$.

3. Implementation Optimizations (REAL vs. Prototype):
   The authors significantly improved upon the original prototype implementation through three main categories of optimization:

   • Data Structures: Implementation of caching and sharing for (sub)formulas, more efficient atom shape normalization, and combining duplicate tree walks to reduce computational overhead.
   • Formula Structure: Direct handling of integer equalities and non-strict real inequalities, sharing common subexpressions in Boolean abstractions, and replacing unnecessary theory variables with Boolean variables to produce more compact formulas.
   • Interoperability: The tool outputs the resulting quantifier-free formula as a standard SMT-LIB file, which can be processed by any SMT solver supporting LIA, LRA, or LIRA (e.g., Z3).

4. Application Pipeline (Alchemist):
   To demonstrate utility in liveness checking, the authors developed Alchemist, a transpiler that converts reachability relations generated by FAST(er) (a tool for verifying reachability in integer counter systems using the Armoise language) into the SMT-LIB format required by REAL. This creates a complete toolchain: Armoise $\to$ FAST(er) $\to$ Alchemist $\to$ REAL $\to$ SMT Solver.

Key Contributions

• The Tool REAL: A solver-agnostic elimination procedure for Ramsey quantifiers that supports LIA, LRA, and LIRA.
• Standardized Input/Output: The first implementation allowing constraints to be specified via an extended SMT-LIB format, removing strict dependencies on specific solver APIs.
• Performance Improvements: A substantial speedup over the original prototype, achieved through optimized data structures and formula generation techniques.
• Liveness Verification Framework: A demonstrated pipeline (Fig. 1) that translates reachability relations from integer counter systems into Ramsey quantifier formulas, enabling automatic liveness verification for parameterized distributed protocols.

Experimental Results

Experiments were conducted on an Arch Linux machine using Z3 v4.15.1 for satisfiability checking.

• Case Studies: The tool successfully verified liveness for several benchmarks, including the McCarthy 91 function, Sliding Window Protocol, Lamport's Bakery Algorithm, and various Cache Coherence protocols (Berkeley, Dragon, MOESI, SYNAPSE, futurbus).
  • For the McCarthy 91 function, REAL successfully verified the absence of infinite cliques, proving termination.
  • For the Lamport Bakery algorithm, the tool correctly identified that verifying the absence of an infinite clique starving one process fails without fairness assumptions.
• Performance Metrics:
  • Scalability: Elimination time scales almost linearly with problem dimension across various benchmark families (Sorted Chain, Average, Cyclic Dependency, Bounding Box). Formulas with thousands of atoms and variables were processed in sub-second to low-second ranges.
  • Comparison with Prototype: REAL outperforms the original prototype by several magnitudes in both elimination and solving times (Fig. 5). In some integer cases, the generated output is so simple that the solver's time exceeds the elimination time.
  • Formula Size: REAL produces significantly more compact formulas compared to the prototype, reducing the number of tree nodes in the output SMT formulas (Fig. 3).

Significance and Claims

The paper claims that REAL provides a modular and efficient verification pipeline for infinite-state systems. By bridging the gap between theoretical elimination algorithms and practical SMT-based verification, it enables the automatic checking of liveness properties that were previously difficult to express or solve.

The authors note that while the approach is effective, the mixed linear integer real arithmetic (LIRA) case still incurs substantial overhead compared to pure LIA or LRA due to the current separation of integer and real variables. They suggest that future work could involve replacing FASTer with tools that directly target reachability relations or streamlining the pipeline to reduce SMT encoding redundancy. The paper concludes that the current implementation successfully extends the capabilities of existing tools like FASTer to handle liveness checking for parameterized distributed protocols.