线性规划渐近非终止初值的生成
Generating Asymptotically Non-Terminating Initial Values for Linear Programs
摘要：
提出了线性循环规划的渐近非终止初始变量值的概念。这些值直接与初始变量值相关联，对于这些初始变量值，相应的程序不会终止。我们的理论贡献为我们提供了强大的计算方法，自动生成一套渐近非终止的初始变量值。这样的集合由半线性空间符号地和精确地表示，例如，以线性等式和不等式的合取和析取为特点。此外，通过取它们的补码，我们得到了程序终止的输入集的精确欠近似。然后我们可以把线性规划的终止问题归结为一组特定的渐近非终止初始变量值的空性检查。我们的静态输入数据分析不仅限于程序中的变量解释的实数。我们扩展了我们的方法，并提供了新的可判定性结果的仿射整数和理性规划的终止问题。
英文摘要：
We present the notion of asymptotically non-terminating initial variable values for linear loop programs. Those values are directly associated to initial variable values for which the corresponding program does not terminate. Our theoretical contributions provide us with powerful computational methods for automatically generating sets of asymptotically non-terminating initial variable values. Such sets are represented symbolically and exactly by a semi-linear space, e.g., characterized by conjunctions and disjunctions of linear equalities and inequalities. Moreover, by taking their complements, we obtain a precise under-approximation of the set of inputs for which the program does terminate. We can then reduce the termination problem of linear programs to the emptiness check of a specific set of asymptotically non-terminating initial variable values. Our static input data analysis is not restricted only to programs where the variables are interpreted over the reals. We extend our approach and provide new decidability results for the termination problem of affine integer and rational programs.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
