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

摘要

In contrast to their reliable and lossy-error counterparts whose termination problems are either undecidable or non-primitive recursive, the termination problem for counter machines with incrementing errors is shown to be ExpSpace-complete. It is also shown that the structural termination problem—deciding whether every run terminates from any starting configuration—for counter machines with incrementing errors is similarly ExpSpace-complete. This stands in marked contrast to both reliable and lossy counter machines, for which the problem is undecidable. The ExpSpace-hardness proof contained herein requires an unbounded supply of counters. Indeed, by fixing the number of available counters, optimal NLogSpace-complete bounds for both the termination and structural termination problems are obtained.