Lexicographic Ranking SuperMartingale (LexRSM) is a generalization of Ranking SuperMartingale (RSM) that offers sound and efficient algorithms for verifying almost-sure termination of probabilistic programs. LexRSM is also a probabilistic counterpart of Lexicographic Ranking Function (LexRF), which verifies termination of non-probabilistic programs. Among the latter, Bradley-Manna-Sipma LexRF (BMS-LexRF) is known for its better applicability. In this paper, we introduce the first variant of LexRSM that instantiates BMS-LexRF. To carve out the LexRSM conditions we propose, an in-depth analysis about the treatment of non-negativity of LexRSM is performed. Our soundness result extends the existing one to a wider class of LexRSMs. A synthesis algorithm of the proposed LexRSM is also given; experiments show the algorithm's advantage on its applicability compared with existing ones.

翻译：词汇排序超鞅（Lexicographic Ranking SuperMartingale, LexRSM）是排序超鞅（RSM）的推广，为验证概率程序几乎必然终止提供了可靠且高效的算法。LexRSM 也是词汇排序函数（Lexicographic Ranking Function, LexRF）的概率对应物，后者用于验证非概率程序的终止。在非概率方法中，Bradley-Manna-Sipma LexRF（BMS-LexRF）以其更广泛的应用性而著称。本文首次提出了一种实例化 BMS-LexRF 的 LexRSM 变体。为精确刻画所提出的 LexRSM 条件，我们对 LexRSM 非负性处理进行了深入分析。我们的正确性结果将现有理论拓展至更广泛的 LexRSM 类别。此外，本文还给出了所提 LexRSM 的合成算法；实验表明，与现有方法相比，该算法在应用范围上具有优势。