a uniform upper bound for these ascending chains. This implies the decidability of termination problem of the family of MPPs. Similar argument is applicable to polynomial guarded commands in which all test guards are polynomial equations.

Related work {#related-work .unnumbered}
------------

In the past, various well-established work on termination analysis can only be applied to linear programs, whose guards and assignments are linear. For single-path linear programs, Colón and Sipma utilized polyhedral cones to synthesize linear ranking functions [@colon:synthesis]. Podelski and Rybalchenko, based on Farkas’ lemma, presented a complete method to find linear ranking functions if they exist [@podelski:ranking]. In [@Ben-AmramG14], Ben[-]{}Amram and Genaim considered to extend the above results in the following two aspects: firstly, they proved that synthesizing linear ranking functions for single path linear programs is still decidable if program variables are interpreted over integers, but with co-NP complexity, in contrast to PTIME complexity when program variables are interpreted over rationals or reals; secondly, they proposed the notion of *lexicographical ranking function* and a corresponding approach for synthesizing lexicographical ranking functions for dealing with linear programs with multi-path.

In recent years, the termination problem of non-linear programs attracted more attentions as they are omnipresent in safety-critical embedded 