Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Implicit Rankings for Verifying Liveness Properties in First-Order Logic

Raz Lotan, Sharon Shoham

TL;DR

We address liveness verification in first-order logic by introducing implicit rankings that approximate the reduction of a ranking function without explicit definition. An implicit ranking is a pair ($\varphi_{\leq}$, $\varphi_{<}$) that under-approximates conservation and reduction of some ranking function $f$ mapping states to a well-founded partial order, enabling sound FO-based proofs via SMT solvers. The authors develop a rich, compositional toolkit of constructors (Binary, Position-in-Order, Pointwise, Lexicographic, Domain-Pointwise, Domain-Permuted-Pointwise, Domain-Lexicographic) to build complex implicit rankings and prove their soundness for finite domains. They implement these constructors in a Python tool that automatically generates the FO premises and leverages Z3 to verify liveness properties expressed as $ (\bigwedge_i \forall \vec{x} \square \lozenge r_i(\vec{x})) \to \square (p \to \lozenge q) $. Empirical evaluation on Dijkstra-style self-stabilizing protocols (including 3-state and 4-state variants) demonstrates practical, automated verification under finite-domain assumptions, highlighting the method’s scalability and potential to automate challenging liveness proofs in FO settings.

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.

Implicit Rankings for Verifying Liveness Properties in First-Order Logic

TL;DR

We address liveness verification in first-order logic by introducing implicit rankings that approximate the reduction of a ranking function without explicit definition. An implicit ranking is a pair (, ) that under-approximates conservation and reduction of some ranking function mapping states to a well-founded partial order, enabling sound FO-based proofs via SMT solvers. The authors develop a rich, compositional toolkit of constructors (Binary, Position-in-Order, Pointwise, Lexicographic, Domain-Pointwise, Domain-Permuted-Pointwise, Domain-Lexicographic) to build complex implicit rankings and prove their soundness for finite domains. They implement these constructors in a Python tool that automatically generates the FO premises and leverages Z3 to verify liveness properties expressed as . Empirical evaluation on Dijkstra-style self-stabilizing protocols (including 3-state and 4-state variants) demonstrates practical, automated verification under finite-domain assumptions, highlighting the method’s scalability and potential to automate challenging liveness proofs in FO settings.

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.

Paper Structure

This paper contains 34 sections, 1 theorem, 11 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Contributions.
  3. Motivating Examples
  4. Preliminaries
  5. First-Order Logic.
  6. Transition Systems in First-Order Logic.
  7. Well-Founded Partial Orders.
  8. Expressing Ranking in First-Order Logic
  9. Using Ranking for Liveness Proofs
  10. Implicit Ranking
  11. Notation.
  12. Constructions of Implicit Rankings
  13. Base Constructors
  14. Binary Constructor.
  15. Position-in-Order Constructor.
  16. ...and 19 more sections

Key Result

theorem 1

All constructors defined in this section are sound in the sense that (i) if the arguments of a constructor satisfy their assumptions, then the output of the constructor is an implicit ranking (for finite domains if the constructor is finite-domain), and (ii) for constructors that receive implicit ra

Figures (2)

  • Figure 1: Toy Stabilization
  • Figure 2: Toy Stabilization

Theorems & Definitions (16)

  • definition 1: Implicit Ranking
  • theorem 1
  • remark 1
  • proof
  • proof
  • proof
  • proof
  • proof
  • proof
  • proof
  • ...and 6 more