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.

翻译：字典序排序超鞅（LexRSM）是字典序排序函数（LexRF）的概率扩展，后者是一种被广泛接受的程序终止性验证技术。本文首次提出了LexRF在更弱的非负性条件（称为单分量非负性）下的可靠概率扩展。已知此类扩展若存在，将因概率情境的复杂性而具有非平凡性。为实现该目标，我们首先设计了可修正性概念，为分析可能为负的LexRSM的可靠性提供了系统化方法。该概念导出了适用于一般随机过程的LexRF理想扩展。接着我们提出另一种称为惰性LexRSM的扩展，面向自动化验证应用；该扩展对具有线性算术的概率程序可靠，而其子类可通过线性规划实现自动化合成。最后我们针对该子类提出了LexRSM合成算法，并进行了实验验证。