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.
Chapter PDF
Similar content being viewed by others
References
Arrowsmith, D.K., Place, C.M.: An introduction to dynamical systems. Cambridge (1990)
Bachmair, L., Dershowitz, N.: Commutation, transformation, and termination. In: Siekmann, J.H. (ed.) CADE 1986. LNCS, vol. 230, pp. 5–20. Springer, Heidelberg (1986)
Blondel, V.D., Bournez, O., Koiran, P., Papadimitriou, C.H., Tsitsiklis, J.N.: Deciding stability and mortality of piecewise affine dynamical system. Theoretical Computer Science 255(1–2), 687–696 (2001)
Blondel, V.D., Tsitsiklis, J.N.: A survey of computational complexity results in systems and control. Automatica 36, 1249–1274 (2000)
Colón, M.A., Sipma, H.B.: Synthesis of linear ranking functions. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 67–81. Springer, Heidelberg (2001)
Colón, M.A., Sipma, H.B.: Practical methods for proving program termination. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 442–454. Springer, Heidelberg (2002)
Dams, D., Gerth, R., Grumberg, O.: A heuristic for the automatic generation of ranking function. In: Workshop on Advances in Verification WAVe 2000, pp. 1–8 (2000)
Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall PTR, Englewood Cliffs (1997)
Hoffman, K., Kunze, R.: Linear Algebra, 2nd edn. Prentice-Hall, Englewood Cliffs (1971)
Kannan, R., Lipton, R.J.: Polynomial-time algorithm for the orbit problem. J. of the ACM 33(4), 808–821 (1986)
Lafferriere, G., Pappas, G.J., Yovine, S.: Symbolic reachability computations for families of linear vector fields. J. Symbolic Computation 32(3), 231–253 (2001)
Musset, J., Rusinowitch, M.: Computing metatransitions for linear transition systems. In: 12th Intl. FME symposium (2003)
Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 239–251. Springer, Heidelberg (2004)
Podelski, A., Rybalchenko, A.: Transition invariants. In: Logic in Computer Science, LICS, IEEE Computer Society, Los Alamitos (2004)
Smart, D.R.: Fixed Point Theorems. Cambridge University Press, Cambridge (1980)
Sontag, E.: From linear to nonlinear: Some complexity comparisons. In: 34th IEEE Conf. on Decision and Control, CDC (1995)
Tiwari, A.: Approximate reachability for linear systems. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 514–525. Springer, Heidelberg (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Tiwari, A. (2004). Termination of Linear Programs. In: Alur, R., Peled, D.A. (eds) Computer Aided Verification. CAV 2004. Lecture Notes in Computer Science, vol 3114. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27813-9_6
Download citation
DOI: https://doi.org/10.1007/978-3-540-27813-9_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22342-9
Online ISBN: 978-3-540-27813-9
eBook Packages: Springer Book Archive