线性约束循环的排序函数
Ranking Functions for Linear-Constraint Loops
AI总结：
本文研究整数变量线性约束循环中线性及字典序线性排序函数的存在性问题，证明一般情形为 coNP 完全，识别 PTIME 特例并给出完整综合算法。
摘要：
本文研究以下问题的复杂性：给定一个由有限变量集合上的线性约束描述的循环，该循环是否存在线性或字典序线性排序函数？虽然此类函数的存在意味着终止，但这些问题并不等价于终止。当变量取值于有理数（或实数）时，已知两个问题均可在 PTIME 时间内判定。然而，当变量取值于整数时，无论是单路径还是多路径循环，其复杂性此前尚未确定。我们证明这两个问题均为 coNP 完全。但我们也指出若干具有 PTIME 复杂性的重要特殊情形。我们还给出了用于综合线性与字典序线性排序函数的完整算法，涵盖一般情形以及 PTIME 特殊情形。此外，在有理数设置下，我们用于综合字典序线性排序函数的算法扩展了现有算法，因为我们的排序函数类别更具一般性，同时仍具有多项式时间复杂性。
英文摘要：
In this paper we study the complexity of the problems: given a loop, described by linear constraints over a finite set of variables, is there a linear or lexicographical-linear ranking function for this loop? While existence of such functions implies termination, these problems are not equivalent to termination. When the variables range over the rationals (or reals), it is known that both problems are PTIME decidable. However, when they range over the integers, whether for single-path or multipath loops, the complexity has not yet been determined. We show that both problems are coNP-complete. However, we point out some special cases of importance of PTIME complexity. We also present complete algorithms for synthesizing linear and lexicographical-linear ranking functions, both for the general case and the special PTIME cases. Moreover, in the rational setting, our algorithm for synthesizing lexicographical-linear ranking functions extends existing ones, because our class of ranking functions is more general, yet it has polynomial time complexity.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
