2026-07-23T08:35:11Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:16297 2024-03-06T10:57:10Z ddc:004 open_access

Certified Decision Procedures for Two-Counter Machines Dudenhefner, Andrej constructive mathematics computability theory decidability counter automata mechanization Coq 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Andrej Dudenhefner 2022 Is Part Of LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2022.16 urn:nbn:de:0030-drops-162978 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.16 eng https://creativecommons.org/licenses/by/4.0/legalcode