systems. Bradley et al. proposed an approach to proving termination of MPPs with polynomial behaviour over $\mathbb{R}$ through finite difference trees [@bradley:polynomial]. Similar idea was used in [@cook:polynomial] for termination analysis of polynomial programs. Typically, with the development of computer algebra, more and more techniques from symbolic computation, for instance, Gröbner basis [@sank:GB; @muller:invariants], quantifier elimination [@kapur:QE] and recurrence relation [@rodriguez:simple; @kovacs:psolvable], are borrowed and successfully applied to the verification of programs. Certainly, these techniques can also be applied to polynomial programs to discover termination or non-termination proofs. Chen et al. proposed a relatively complete (w.r.t. a given template) method for generating polynomial ranking functions over $\mathbb{R}$ by reduction to semi-algebraic system solving [@chen:ranking]. Gupta et al. proposed a practical method to search for counter-examples of termination [@gupta:NT], by first generating lasso-shaped [@cook:code] candidate paths and then checking the feasibility of the “lassoes" using constraint solving. Velroyen and Rümmer applied invariants to show that terminating states of a program are unreachable from certain initial states, and then identified these “bad” initial states by constraint-solving [@Velroyen08]. Brockschmidt et al. detected non-termination and Null Pointer Exceptions for by constructing and analyzing termination graphs, and implemented a termination prover [@Brockschmidt11].

For more general 