programs, many other techniques, like predicate abstraction, parametric abstraction, fair assumption, Lagrangian relaxation, semidefinite programming, sum of squares, etc., have been successfully applied [@cousot:termination; @cousot:lagrangian; @cook:conditional].

The following work are more related to ours. Tiwari first identified a class of simple linear loops and proved that its termination problem is decidable over reals $\mathbb{R}$ [@tiwari:terminate]. Braverman extended Tiwari’s result by proving the termination problem is still decidable when program variables are interpreted over integers $\Bbb{Z}$ [@braverman:terminate], and Xia and Zhang investigated an extension of Tiwari’s simple linear loops by allowing a loop condition to be non-linear constraint and proved that the termination problem of the extension is still decidable over reals, and becomes undecidable over integers [@XZ2010]. In [@bradley:polynomial], Brandley et al. proved that the termination problem of MPPs with inequalities as loop conditions is not semi-decidable. Additionally, Müller-Olm and Seidl proved that the termination problem of linear guarded commands with equations and inequations as guards is undecidable [@Muller-Olm]. Thus, we believe that the class of polynomial programs, i.e., polynomial guarded commands with equalities as guards, under consideration in this paper, is the largest one with a decidable termination problem, any extension of it by allowing inequalities, or inequations in 