Lexicographic Ranking Supermartingales with Lazy Lower Bounds

TL;DR

This work addresses the challenge of extending Lexicographic Ranking Functions to probabilistic programs under the weakest practical non-negativity constraints. It introduces fixable LexRSMs, including $\varepsilon$-fixable and $(\varepsilon,\gamma)$-fixable variants, and shows they yield SC-LexRF instantiations and AST guarantees, with GLexRSM shown to be a special case. To enable automated synthesis, the authors propose Lazy LexRSM (LLexRSM) and an LP-based subclass using a multiple-choice leftward condition (MCLC), along with theoretical guarantees of soundness under linearity and well-behaved distributions. An iterative synthesis algorithm and experimental evaluation demonstrate that relaxing non-negativity via LLexRSM and fixability significantly broadens the set of verifiable probabilistic programs, outperforming prior STR/LW-based approaches in many benchmarks. The results provide a practical framework for automated termination verification in probabilistic settings and open questions about distribution classes and completeness of synthesis variants.

Abstract

Lexicographic Ranking SuperMartingale (LexRSM) is a probabilistic extension of Lexicographic Ranking Function (LexRF), which is a widely accepted technique for verifying program termination. In this paper, we are the first to propose sound probabilistic extensions of LexRF with a weaker non-negativity condition, called single-component (SC) non-negativity. It is known that such an extension, if it exists, will be nontrivial due to the intricacies of the probabilistic circumstances. Toward the goal, we first devise the notion of fixability, which offers a systematic approach for analyzing the soundness of possibly negative LexRSM. This notion yields a desired extension of LexRF that is sound for general stochastic processes. We next propose another extension, called Lazy LexRSM, toward the application to automated verification; it is sound over probabilistic programs with linear arithmetics, while its subclass is amenable to automated synthesis via linear programming. We finally propose a LexRSM synthesis algorithm for this subclass, and perform experiments.

Figures (6)

• Figure 1: A demo of different non-negativity conditions for LexRFs. There, the ranking dimensions of the LexRF $\boldsymbol{\eta}$ are indicated by underlines, and the last column of the table shows where each condition requires $\boldsymbol{\eta}$ to be non-negative.
• Figure 2: A probabilistic modification of speedDis1alias2010multi, where $\mathit{Unif}[a,b]$ is a uniform sampling from the (continuous) interval $[a,b]$. Inequalities on the right represent invariants. While $\boldsymbol{\eta}$ is not a GLexRSM, it is an LLexRSM we propose; thus it witnesses almost-sure termination of the program.
• Figure 3: An example of "ill" exploitation.
• Figure 4: An example of "harmless" unbounded negativity.
• Figure 5: The syntax of probabilistic programs

Theorems & Definitions (11)

• proof
• proof
• remark 1
• proof : sketch
• proof
• proof
• proof
• proof
• proof
• proof