About the decision of reachability for register machines
RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 36 (2002) no. 4, pp. 341-358.

We study the decidability of the following problem: given $p$ affine functions ${f}_{1},...,{f}_{p}$ over ${ℕ}^{k}$ and two vectors ${v}_{1},{v}_{2}\in {ℕ}^{k}$, is ${v}_{2}$ reachable from ${v}_{1}$ by successive iterations of ${f}_{1},...,{f}_{p}$ (in this given order)? We show that this question is decidable for $p=1,2$ and undecidable for some fixed $p$.

DOI : https://doi.org/10.1051/ita:2003001
Classification : 68Q60
Mots clés : verification, infinite state systems
@article{ITA_2002__36_4_341_0,
author = {Cortier, V\'eronique},
title = {About the decision of reachability for register machines},
journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
pages = {341--358},
publisher = {EDP-Sciences},
volume = {36},
number = {4},
year = {2002},
doi = {10.1051/ita:2003001},
zbl = {1034.68057},
mrnumber = {1965421},
language = {en},
url = {www.numdam.org/item/ITA_2002__36_4_341_0/}
}
Cortier, Véronique. About the decision of reachability for register machines. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 36 (2002) no. 4, pp. 341-358. doi : 10.1051/ita:2003001. http://www.numdam.org/item/ITA_2002__36_4_341_0/

[1] E. Asarin, G. Schneider and S. Yovine, Towards computing phase portraits of polygonal differential inclusions, in HSCC'2002, Hybrid Systems: Computation and Control. Stanford, USA, Lecture Notes in Comput. Sci. 2289 (2002) 49-61. | Zbl 1054.93030

[2] B. Boigelot, Symbolic Methods for Exploring Infinite Sate Spaces, Ph.D. Thesis. Université de Liège (1998) 225.

[3] H. Comon and Y. Jurski, Multiple counters automata, safety analysis and Presburger arithmetic, in Proc. Computer Aided Verification. Springer Verlag, Lecture Notes in Comput. Sci. 1427 (1998) 268-279. | MR 1729041

[4] V. Cortier, Vérification de systèmes à compteurs (in French), Master's Thesis. Université Paris 7 (1999) http://www.lsv.ens-cachan.fr/$\sim$cortier/memoire_dea.ps

[5] L.E. Dickson, Finiteness of the odd perfect and primitive abundant numbers with $n$ distinct prime factors. Amer. J. Math. 35 (1913) 413-422. | JFM 44.0220.02 | MR 1506194

[6] C. Dufourd, A. Finkel and Ph. Schnoebelen, Between decidability and undecidability, in Proc. ICALP 1998. Springer-Verlag, Lecture Notes in Comput. Sci. 1448 (1998) 103-115. | MR 1683488 | Zbl 0909.68124

[7] A. Finkel, P. Mckenzie and C. Picaronny, A well-structured framework for analysing Petri nets extensions. Technical Report, Research Report LSV-99-2 (1999) http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/rr-lsv-1999-2.rr.ps | Zbl 1101.68696

[8] M.Yu. Matijacevitch, M. David and J. Robinson, Hilbert's Tenth Problem, Chapter 3 (1976). | Zbl 0346.02026

[9] C. Rorres and H. Anton, Applications of Linear Algebra, Chapters 9 and 13 (1979). | Zbl 0439.15001