基于 Positivstellensatz 的概率程序终止分析

我们考虑具有最基本活性性质——终止性的非确定性概率程序。我们提出了针对具有多项式守卫和赋值的非确定性概率程序进行终止分析的高效方法。我们的方法通过综合多项式秩上鞅来实现，该方法一方面显著推广了线性秩上鞅，另一方面是非概率程序终止性证明中多项式秩函数的对应物。该方法通过 Positivstellensatz 综合多项式秩上鞅，产生了一种高效方法，该方法不仅可靠，而且在一大类程序子类上半完备。我们展示了实验结果，证明我们的方法能够处理几个具有复杂多项式守卫和赋值的经典程序，并且即使在简单仿射程序中不存在线性秩上鞅时，也能综合出高效的二次秩上鞅。