When the tools in I4: Incremental inference of inductive invariants for verification of distributed protocols and On Symmetry and Quantification: A New Approach to Verify Distributed Protocols search for an inductive invariant of a distributed system, the search procedure instantiates a series of small finite models and tries to infer from their truth tables a series of logical formulae that hold over those finite models. These formulae are found by running the Quine-McCluskey algorithm for minimization of Boolean functions. The prime implicants found by Quine-McCluskey have a latent symmetry that can be abstracted into quantified formulae. There are only so many small numbers, and so small finite models may propose formulae that do not hold at larger sizes. However, if you find a formula that holds at size $𝑛$ as well as size $𝑛+1$, then it is likely a good candidate to hold at all sizes. You need to be a little careful if your protocol is indexed by several variables, but mostly this general idea holds when abstracting to a protocol of unbounded size. Further discussion of this idea can be found in SAT-based quantified symmetric minimization of the reachable states of distributed protocols: An update.

My observation was that Quine-McCluskey is just a special instance of Buchberger’s algorithm for computing Gröbner Bases. That is, you can describe Boolean formulae as polynomials over the field with two elements, and in this translation Quine-McCluskey and Buchberger each compute the same data. This observation isn’t new in and of itself, but it does open up an opportunity to generalize the invariant search procedure that is used above.

The place I went looking to apply this idea was in the search of polynomial loop invariants. If a loop had an invariant that is expressible as a polynomial relation between the program variables, then you could apply the same idea as above to infer the loop invariant.

Suppose ${𝑥}_1,\dots ,{𝑥}_{𝑛}$ are the variables in scope of program $𝑆$ and $𝑆$ contains a loop that we want to infer an invariant for. Denote the value of ${𝑥}_{𝑖}$ at the $𝑗$-th loop iteration by ${𝑥}_{𝑖,𝑗}$. The invariant search procedure proceeds intuitively as the following: we will keep track of the minimal set of polynomials that could interpolate between all of the variable assignments that we have witnessed thus far. Formally this is kept track of by the ideal of polynomials. At the $𝑗$-th loop iteration we add a new generator to the ideal which corresponds to the assignments ${𝑥}_{1,𝑗},\dots ,{𝑥}_{𝑛,𝑗}$. The Gröbner basis for this ideal provides the minimal data needed to generate all the assignments witnessed thus far, so if this process saturates then the Gröbner basis encodes a polynomial loop invariant. The nice thing about polynomials is that they have finite degree which guarantees that this process does indeed saturate (provided that the degree of the invariant is smaller than the number of loop iterations).

I was so excited to find this idea. I’d felt like it was my first good idea in grad school. Then I read Automatic Generation of Polynomial Loop Invariants: Algebraic Foundations and found out someone had done this 20 years ago. I still wonder from time to time if there is room to further refine this idea or perhaps further generalize it. For instance, there is further generalization beyond Quine-McCluskey or Buchberger to the Knuth-Bendix algorithm, which seems to be a more general instance of both of these algorithms. So perhaps this search procedure can be weakened to an even more general class? Although, I’m not yet familiar much with the Knuth-Bendix algorithm.