Termination of Linear Programs

We show that termination of a class of linear loop programs is decidable. Linear loop programs are discrete-time linear systems with a loop condition governing termination, that is, a while loop with linear assignments. We relate the termination of such a simple loop, on all initial values, to the eigenvectors corresponding to only the positive real eigenvalues of the matrix defining the loop assignments. This characterization of termination is reminiscent of the famous stability theorems in control theory that characterize stability in terms of eigenvalues.

• Type: Conference
• Year: 2004
• Where: CAV
• Authors: Ashish Tiwari
• Keywords: CAV 2004, Condition Governing Termination, Discrete-time Linear Systems, Formal Methods, Linear Loop Programs