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

Article type: Research Article

Authors: Ben-Amram, Amir M.

Affiliations: The Academic College of Tel Aviv-Yaffo, Israel. E-mail: amirben@cs.mta.ac.il; Url: www2.mta.ac.il/~amirben

Abstract: 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 Rn. 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 x0,f(x0),f(f(x0)),…) 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 Rn (or Qn), 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 Π02 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.

Keywords: Piecewise-affine functions, termination, mortality, convergence, undecidability

DOI: 10.3233/COM-150032

Journal: Computability, vol. 4, no. 1, pp. 19-56, 2015