to decide even for linear loops, since such problem is equivalent to the famous Skolem’s problem [@OW15]. On the other hand, inequality loop guards can be strengthened as equality guards, e.g. $f(x)\neq 0\Leftarrow f(x)z+1=0$, thus our approach can also be used to find non-terminating inputs for general MPPs.

The basic idea of our approach is as follows: Given an MPP $P$ with $\ell$ paths, for any input ${\pmb{x}}\in \mathbb{R}^d$, if at the first iteration ${\pmb{x}}$ satisfies the loop guard, then one of the paths in the loop body will be nondeterministically selected and the corresponding assignment will be used to update the value of ${\pmb{x}}$, which results in $\ell$ possible values of ${\pmb{x}}$; afterwards, the above procedure is repeated until the guard does not hold any more. Thus the execution of an MPP on input ${\pmb{x}}\in \mathbb{R}^d$ forms a tree. An input ${\pmb{x}}$ is called *non-terminating* if the execution tree on ${\pmb{x}}$ has an infinite path. Obviously, each of such paths forms an ascending chain of polynomial ideals, and an input ${\pmb{x}}$ is *non-terminating* iff ${\pmb{x}}$ is in the variety of an ascending chain in the execution tree. By using some results of polynomial algebra, we prove that there is 