简单线性循环：代数不变量与应用
Simple Linear Loops: Algebraic Invariants and Applications
AI总结：
本文提出一种多项式空间算法计算简单线性循环的最强代数不变量，并探讨了其在不变量验证与循环综合中的应用及复杂度。
摘要：
循环不变量的自动生成是软件验证中的一个基本挑战。虽然该任务在一般情况下是不可判定的，但对于某些受限类别的程序，它是可判定的。本工作专注于具有单一线性更新的（无分支）循环的不变量生成。\n 我们的主要贡献是一个多项式空间算法，该算法计算简单线性循环的最强代数不变量，生成在所有可达状态下的程序变量之间成立的所有多项式方程。实现我们复杂度界限的关键在于缓解变量消除和Gröbner基计算相关的爆炸问题，正如先前工作中所见。当程序变量数量固定时，我们的过程在多项式时间内运行。\n 我们研究了不变量生成结果的各种应用，重点关注不变量验证和循环综合。不变量验证问题研究定义代数集的多项式理想是否作为给定线性循环的不变量。我们证明，当输入理想分别以稠密或稀疏表示给出时，该问题是coNP完全的，并且属于PSPACE。在循环综合的背景下，我们的目标是构造一个具有无限可达状态集的循环，该循环将指定的代数性质作为不变量来维护。该问题的强综合变体要求构造循环，使得给定性质是最强不变量。在硬度方面，在整数（或有理数）上综合循环与希尔伯特第十问题（或其在有理数上的类比）一样困难。当输出的常数被限制为位数有界的有理数时，我们证明循环综合及其强变体在PSPACE中都是可判定的，并且当程序变量数量固定时在NP中。
英文摘要：
The automatic generation of loop invariants is a fundamental challenge in software verification. While this task is undecidable in general, it is decidable for certain restricted classes of programs. This work focuses on invariant generation for (branching-free) loops with a single linear update. Our primary contribution is a polynomial-space algorithm that computes the strongest algebraic invariant for simple linear loops, generating all polynomial equations that hold among program variables across all reachable states. The key to achieving our complexity bounds lies in mitigating the blowup associated with variable elimination and Gröbner basis computation, as seen in prior works. Our procedure runs in polynomial time when the number of program variables is fixed. We examine various applications of our results on invariant generation, focusing on invariant verification and loop synthesis. The invariant verification problem investigates whether a polynomial ideal defining an algebraic set serves as an invariant for a given linear loop. We show that this problem is coNP-complete and lies in PSPACE when the input ideal is given in dense or sparse representations, respectively. In the context of loop synthesis, we aim to construct a loop with an infinite set of reachable states that upholds a specified algebraic property as an invariant. The strong synthesis variant of this problem requires the construction of loops for which the given property is the strongest invariant. In terms of hardness, synthesising loops over integers (or rationals) is as hard as Hilbert's Tenth problem (or its analogue over the rationals). When the constants of the output are constrained to bit-bounded rational numbers, we demonstrate that loop synthesis and its strong variant are both decidable in PSPACE, and in NP when the number of program variables is fixed.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
