Implicit Rankings for Verifying Liveness Properties in First-Order Logic

TL;DR

This paper introduces implicit rankings, a novel first-order logic approach to verify liveness properties, enabling automation in complex systems where explicit ranking functions are hard to reason about.

Contribution

The paper presents a new concept of implicit rankings with recursive constructors that approximate ranking functions, enhancing automated verification in first-order logic.

Findings

Successfully verified complex liveness properties

Demonstrated effectiveness on self-stabilizing protocols

Extended reasoning capabilities with quantifier-based constructors

Abstract

Liveness properties are traditionally proven using a ranking function that maps system states to some well-founded set. Carrying out such proofs in first-order logic enables automation by SMT solvers. However, reasoning about many natural ranking functions is beyond reach of existing solvers. To address this, we introduce the notion of implicit rankings - first-order formulas that soundly approximate the reduction of some ranking function without defining it explicitly. We provide recursive constructors of implicit rankings that can be instantiated and composed to induce a rich family of implicit rankings. Our constructors use quantifiers to approximate reasoning about useful primitives such as cardinalities of sets and unbounded sums that are not directly expressible in first-order logic. We demonstrate the effectiveness of our implicit rankings by verifying liveness properties of several intricate examples, including Dijkstra's k-state, 4-state and 3-state self-stabilizing protocols.