Mortality of iterated piecewise affine functions over the integers: Decidability and complexity

摘要

In the theory of discrete-time dynamical systems one studies the limiting behaviour of processes defined by iterating a fixed function f over a given space. An important special case involves piecewise affine functions on R~n. Blondel et al., in: Theor. Comput. Sci. 255(1, 2) (2001), 687-696, studied the decidability of questions such as global convergence and mortality for such functions with rational coefficients. Mortality means that every trajectory (namely a sequence x_0, f(x_0), f(f(x_0)),...)includes a 0; if the iteration is implemented as a loop while (x ≠ 0) x:= f(x), mortality means that the loop is guaranteed to terminate. Checking the termination of simple loops (under various restrictions of the guard and the update function) is a much-studied topic in automated program analysis. Blondel et al. proved that the problems are undecidable when the state space is R~n (or Q~n), and the dimension n is at least two. From a program analysis (and discrete computability) viewpoint, it is more natural to consider functions over the integers. This paper establishes (un)decidability results for the integer setting, while strengthening results for the continuous setting. We show that also over integers, undecidability begins at two dimensions. In both settings, we shown ∏_2~0 completeness. We further investigate the effect of several restrictions on the iterated functions. Specifically, we consider bounding the size of the partition defining f, and restricting the coefficients of the linear components. In the decidable cases, we give complexity results: The problem is PSPACE-complete for piecewise-affine functions in one dimension; it is polynomial-time for affine functions in any dimension. The undecidability proofs use some variants of the Collatz problem, which may be of independent interest.