License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2022.16
URN: urn:nbn:de:0030-drops-162978
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16297/
Dudenhefner, Andrej
Certified Decision Procedures for Two-Counter Machines
Abstract
Two-counter machines, pioneered by Minsky in the 1960s, constitute a particularly simple, universal model of computation. Universality of reversible two-counter machines (having a right-unique step relation) has been shown by Morita in the 1990s. Therefore, the halting problem for reversible two-counter machines is undecidable. Surprisingly, this statement is specific to certain instruction sets of the underlying machine model.
In the present work we consider two-counter machines (CM2) with instructions inc_c (increment counter c, go to next instruction), dec_c q (if counter c is zero, then go to next instruction, otherwise decrement counter c and go to instruction q). While the halting problem for CM2 is undecidable, we give a decision procedure for the halting problem for reversible CM2, contrasting Morita’s result.
We supplement our result with decision procedures for uniform boundedness (is there a uniform bound on the number of reachable configurations?) and uniform mortality (is there a uniform bound on the number of steps in any run?) for CM2.
Termination and correctness of each presented decision procedure is certified using the Coq proof assistant. In fact, both the implementation and certification is carried out simultaneously using the tactic language of the Coq proof assistant. Building upon existing infrastructure, the mechanized decision procedures are contributed to the Coq library of undecidability proofs.
BibTeX - Entry
@InProceedings{dudenhefner:LIPIcs.FSCD.2022.16,
author = {Dudenhefner, Andrej},
title = {{Certified Decision Procedures for Two-Counter Machines}},
booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
pages = {16:1--16:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-233-4},
ISSN = {1868-8969},
year = {2022},
volume = {228},
editor = {Felty, Amy P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/16297},
URN = {urn:nbn:de:0030-drops-162978},
doi = {10.4230/LIPIcs.FSCD.2022.16},
annote = {Keywords: constructive mathematics, computability theory, decidability, counter automata, mechanization, Coq}
}
