Non-termination Analysis of Linear Loop Programs with Conditionals

摘要

Non-termination analysis of loop programs plays a central role in many applications, especially in the field of safety critical softwares. This paper presents a method to analyze non-termination of linear programs with conditionals. We transform the linear loop programs with conditionals into the nested linear loop programs, and then check whether the inner loop terminates or not by the positive eigenvalues and their corresponding eigenvectors. If one of the inner loop in the nested linear loop is non-terminating, then the linear loop is non-terminating. Otherwise, we need to use ranking function or finite differences of expressions over transition systems to analyze the termination of the outer loop.