单调约束迁移系统的有界终止性
Bounded Termination of Monotonicity-Constraint Transition Systems
摘要：
直觉上，如果我们能证明一个程序终止，我们期望得到一些关于它的复杂性的结论。但是，从终止证明到复杂性界限的过程并不总是清楚的。在这项工作中，我们考虑单调性约束过渡系统，一个程序抽象的终止是可判定的（基于大小变化终止原则）。我们表明，这些程序也有一个可判定的复杂性属性：可以确定是否所有的过渡序列的长度可以有界的初始状态。这就是有界终止问题。有趣的是，如果存在一个界限，它必须是多项式的。我们证明了有界终止问题是PSPACE-完全的。我们还讨论了，理论上，使用的抽象程序上的界限来推断一个具体的程序，已被抽象的结论。结论可能是一个多项式时间界，或在其他情况下多项式空间或指数时间。我们认为，单调性约束抽象的承诺是有用的程序的实际复杂性分析。
英文摘要：
Intuitively, if we can prove that a program terminates, we expect some conclusion regarding its complexity. But the passage from termination proofs to complexity bounds is not always clear. In this work we consider Monotonicity Constraint Transition Systems, a program abstraction where termination is decidable (based on the size-change termination principle). We show that these programs also have a decidable complexity property: one can determine whether the length of all transition sequences can be bounded in terms of the initial state. This is the Bounded Termination problem. Interestingly, if a bound exists, it must be polynomial. We prove that the bounded termination problem is PSPACE-complete. We also discuss, theoretically, the use of bounds on the abstract program to infer conclusions on a concrete program that has been abstracted. The conclusion maybe a polynomial time bound, or in other cases polynomial space or exponential time. We argue that the monotonicity-constraint abstraction promises to be useful for practical complexity analysis of programs.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
