Abstract
We present a method based on the discriminant sequence and Gröbner bases to verify the termination of a class of linear program. This method relates the program termination to the existence of real zeros of polynomial system with constraint conditions. To avoid the wrong determination due to approximate computation, we use Gröbner bases and revised sign list to count sign changes of characteristic polynomial of a trace matrix. This method need not solve the equations of polynomial system but count the number of real zeros which satisfy the constraint condition by using symbolic computation. The number of real zeros of polynomial in the linear program can always be computed correctly. Therefore, the termination of the program can be decided accurately.
This paper is supported partially by No. 20071311 of Education Committee of Tianjin Municipality. The research is also supported by Talent Foundation in TUTE through grant KYQD06005 and Natural Science Foundation of TUTE under grant No. KJY12-09 and KJ20080039.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Yang, L., Zhan, N., Xia, B., et al. Program verification by Using DISCOVERER. Proc.VSTTE’05, Zurich. (2005)
Tiwari, A.: Termination of Linear Programs, pp. 70–82. CAV’04, USA (2004). LNCS
Yang, L., Xia, B.C.: Automated Proving and Discovery of Inequalities. Science Press, China (2008)
Li, J., Li, Y., Feng, Y.: Termination of a class of nonlinear loop programs. J. Sichuan Univ. (Eng. Sci. Edition) 41(1), 129–133 (2009)
Cox, D.A., Little, J.B., O’Shea, Donald, B.: Using Algebric Geometry. Springer, New York (1998)
Mirshra, B.: Algorithmic Algebra. Springer, New York (1993)
Yang, L., Zhang, J.Z., Hou, X.R.: Nonlinear Algebraic Equation System and Automated Theorem Proving. ShangHai Scientific and Technological Education Publishing House, Shanghai (1996)
Zhou, C.Z.: Formal Techniques for software Embeded System. East-China Normal University, Shanghai (2008)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Li, Y., Song, Y., Wu, Z. (2014). Signature-Based Method of Deciding Program Termination. In: Feng, R., Lee, Ws., Sato, Y. (eds) Computer Mathematics. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-43799-5_22
Download citation
DOI: https://doi.org/10.1007/978-3-662-43799-5_22
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-43798-8
Online ISBN: 978-3-662-43799-5
eBook Packages: Mathematics and StatisticsMathematics and Statistics (R0)