排名超马丁格尔中的公平性
摘要：LexRSM：一种排名次序的超旋律（Lexecographic Ranking SuperMartingale）是排名超旋律（Ranking SuperMartingale，RSM）的一种推广，提供了验证概率程序几乎确定终止的可靠和高效算法。LexRSM也是词典式排名函数（Lexicographic Ranking Function，LexRF）的概率对应，用于验证非概率性程序的终止。在非概率程序中，Bradley-Manna-Sipma词典式排名函数（BMS-LexRF）因其更好的适用性而闻名。本文介绍了LexRSM的第一种变体，即BMS-LexRF的具体化实例。为了诠释我们所提出的LexRSM条件，我们对LexRSM非负性处理进行了深入分析。我们的可靠性结果将现有结果扩展到更广泛的LexRSM类。我们还给出了所提出的LexRSM的综合算法；实验结果表明，与现有算法相比，该算法在适用性上具有优势。
作者：Toru Takisaka, Libo Zhang, Changjiang Wang, Jiamou Liu
论文ID：2304.11363
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-04-25