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.

翻译：传统上，活性属性的证明依赖于将系统状态映射至某良基集的排序函数。在一阶逻辑中完成此类证明可实现SMT求解器的自动化验证。然而，现有求解器难以对许多自然排序函数进行推理。为此，我们提出隐式排序的概念——即能够可靠逼近某排序函数递减性、且无需显式定义该函数的一阶逻辑公式。我们提供可实例化与组合的递归式隐式排序构造器，从而衍生出丰富的隐式排序族。这些构造器通过量词逼近对集合基数、无界求和等一阶逻辑无法直接表达的有用原语的推理。我们通过验证若干复杂案例（包括Dijkstra的k状态、4状态与3状态自稳定协议）的活性属性，证明了所提隐式排序方法的有效性。