用于唯一固定点的超鞅：下界验证的统一方法

许多概率程序的量化属性可表述为最小固定点，但验证其下界仍是一个具有挑战性的问题。我们提出了一种新型下界验证方法，利用并扩展了固定点唯一性与程序终止之间关系的联系。核心技术工具是一种对秩鞅（ranking supermartingales）的推广，作为唯一固定点证据。我们的方法提供了一种简单且统一的推理原则，可适用于广泛的量化属性，包括终止概率、最弱前期望、预期运行时间、运行时间的高阶矩以及条件最弱前期望。我们提供了一种基于模板的算法，用于自动化下界验证，并通过实验演示了所提方法的有效性。