On the termination and structural termination problems for counter machines with incrementing errors (Q2037198)

The central question of this research is to determine whether a counter machine halts when this counter machine makes errors, in dependence on the machine program and the types of errors tolerated. Here, counter machines are machines with finitely many counters that can increment, decrement and zero-test the counters. Furthermore, the instructions are linked to states or line numbers, and after each operation the counter machine goes to a new line number, perhaps in dependence on the outcome of a zero-test of a counter. Counters that are \(0\) cannot be decremented and the machine terminates with an error message. Only runs that perform infinitely many operations without machine errors (like decrementing \(0\)) are assumed to be nonterminating. Two types of errors are considered: incrementing errors where some of the counters of the counter machine spontaneously during a state transition increase their values to an arbitrary number, and lossy counter errors where the counters can during state transitions spontaneously lose value. One distinguishes two types of termination (halting): first, whether the counter machine from the input starting point terminates (here the input is incorporated into the machine description); second, whether the counter machine terminates from every configuration in the configuration space, the latter is called structural termination. Furthermore, with respect to the types of errors, a program is halting if every run in which the errors of the allowed type occur (lossy or incrementing, respectively) halts eventually. This universal quantification makes the question investigated in some cases easier: for example, the termination problem of lossy counter machines is decidable while, when forbidding all errors, the same problem is undecidable and as difficult as the halting problem of Turing machines. The author's contributions are to study the termination for incrementing errors. Prior work showed that if one bounds the number of counters by a constant \(k\), the problem to decide whether a given counter machine halts is complete for nondeterministic logarithmic space. The author shows the same is true for the structural halting problem of counter machines with up to \(k\) counters. However, without bounding the number of counters by \(k\), that is, letting the number of registers be part of the machine description given to the decision procedure, the computational complexity increases for both the termination problem and the structural termination problem from nondeterministic logarithmic space complete to exponential space complete and the author's contribution is to prove the exponential space lower bound; the upper bound was known before in the case of normal termination. Here, completeness for a class (like problems solvable in logarithmic space) means that every further problem in this class can be reduced with a logspace many-one reduction to the given complete problem; furthermore, the problem has to be in the class as well. The results obtained are a bit parallel to the normal termination problem for lossy errors, where prior work showed that bounding the number of registers by a constant \(k\) brings down the complexity from Ackermann complete to some subclass of primitive recursive. In his paper the author gives a detailed overview on the history of the problems and the prior results obtained by other authors; the reader might consult his work for studying the quite comprehensive review of the relevant literature in his introduction.