Fairness in Ranking Supermartingales

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.