Termination of linear programs

Ashish Tiwari

Presented at CAV 2004, Boston, July 12--15 2004, © Springer-Verlag.

Abstract

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.

gzipped postscript or postscript or pdf

Errata: There is an error in Example 3 of the paper.

Slides

First version of the slides of the presentation at CAV'04 are available here in postscript format.

BibTeX Entry


@inproceedings{Tiwari04:CAV,
	TITLE = {Termination of linear programs},
	AUTHOR = {Tiwari, A.},
	BOOKTITLE = {Computer-Aided Verification, CAV},
	EDITOR = "Alur, R. and Peled, D.",
	PAGES = {70--82}
	PUBLISHER = {Springer},
	SERIES = {LNCS},
	VOLUME = "3114",
	MONTH = jul,
	YEAR = 2004
}
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page