带惰性下界的词典序秩上鞅
编程语言
2025-04-14 v2
摘要
词典序秩上鞅（LexRSM）是词典序秩函数（LexRF）的概率扩展，而 LexRF 是一种被广泛接受的验证程序终止性的技术。本文中，我们首次提出具有更弱非负性条件（称为单分量（SC）非负性）的 LexRF 的合理概率扩展。已知此类扩展若存在，由于概率环境的复杂性将是非平凡的。为此，我们首先设计了可修复性（fixability）概念，为分析可能为负值的 LexRSM 的合理性提供了系统性方法。该概念给出了 LexRF 的一个期望扩展，其对一般随机过程合理。我们随后提出另一种扩展，称为惰性 LexRSM（Lazy LexRSM），以应用于自动化验证；它对具有线性算术的概率程序合理，而其子类可通过线性规划进行自动化合成。我们最终针对该子类提出了 LexRSM 合成算法并进行了实验。
引用
@article{arxiv.2304.11363,
title = {Lexicographic Ranking Supermartingales with Lazy Lower Bounds},
author = {Toru Takisaka and Libo Zhang and Changjiang Wang and Jiamou Liu},
journal= {arXiv preprint arXiv:2304.11363},
year = {2025}
}