一类带初始输入的线性循环终止性分析

Termination Analysis of a Class of Initialized Linear Loops

针对带初始输入的2维齐次线性循环的终止性问题进行研究。通过分析该类循环所有非终止点组成集合(即NT集)的性质,将该类循环NT集的构造问题转化为一类非线性优化求解问题,并给出了此类优化问题的数学模型。最终,通过验证该类循环的初始输入是否位于所构造的NT集合内,判定了带初始输入的2维齐次线性循环的终止性,并建立了用来完备判定该类循环终止性的算法。

The termination of the initialized two variable homogeneous linear loops was studied. By analyzing the property of the set NT composed of all nonterminating points,the problem about the construction of NT was converted to a class of nonlinear optimization problem. More importantly,by verifying whether or not the initial input of such loops lies in set NT,the termination of the initialized two variable homogeneous linear loops can be checked completely.