On the termination and structural termination problems for counter machines with incrementing errors
type: Item
instance of: scholarly article
title: On the termination and structural termination problems for counter machines with incrementing errors
zbMATH Open document ID: 1480.68008
author: Christopher Hampson
published in: Journal of Computer and System Sciences
publication date: 2021-06-30T00:00:00Z
review text: 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…
reviewed by: Frank Stephan
Mathematics Subject Classification ID: 68Q04
Mathematics Subject Classification ID: 68Q17
Mathematics Subject Classification ID: 68Q25
zbMATH DE Number: 7365385
zbMATH Keywords: termination
zbMATH Keywords: structural termination
zbMATH Keywords: halting problem
zbMATH Keywords: unreliable counter machines
zbMATH Keywords: incrementing error
zbMATH Keywords: lossy error
MaRDI profile type: Publication
full work available at URL: j.jcss.2021.03.007
OpenAlex ID: W3153709765
cites work: Q5590814
cites work: Undecidable problems in unreliable computations.
cites work: Verifying programs with unreliable channels
cites work: Unreliable channels are easier to verify than perfect channels
cites work: Using forward reachability analysis for verification of lossy channel systems
cites work: Revisiting Ackermann-Hardness for Lossy Counter Machines and Reset Petri Nets
cites work: Complexity hierarchies beyond elementary
cites work: The complexity of decision procedures in relevance logic II
cites work: LTL with the freeze quantifier and register automata
cites work: Foundations of Software Science and Computation Structures
cites work: On the decidability and complexity of Metric Temporal Logic over finite words
cites work: On termination and invariance for faulty channel machines
cites work: On the termination problem for counter machines with incrementing errors
cites work: Computability and complexity theory.
cites work: Counter machines and counter languages
cites work: Undecidable Propositional Bimodal Logics and One-Variable First-Order Linear Temporal Logics with Counting
cites work: Lossy Counter Machines Decidability Cheat Sheet
DOI: 10.1016/J.JCSS.2021.03.007
Recommended article: On the termination problem for counter machines with incrementing errors
Recommended article: On termination and invariance for faulty channel machines
Recommended article: Q4536378
Recommended article: The Well Structured Problem for Presburger Counter Machines
Recommended article: On Termination for Faulty Channel Machines
Recommended article: Unboundedness problems for machines with reversal-bounded counters
Recommended article: Terminating Turing Machine Computations and the Complexity and/or decidability of Correspondence Problems, Grammars, and Program Schemes
Recommended article: Boundedness problems for Minsky counter machines
Recommended article: On the Computational Content of Termination Proofs
description: scientific article; zbMATH DE number 7365385