About the decision of reachability for register machines

Cortier, Véronique

doi:10.1051/ita:2003001

Cortier, Véronique

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 36 (2002) no. 4, pp. 341-358.

Résumé

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$ .

MR Zbl

DOI : 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},
     mrnumber = {1965421},
     zbl = {1034.68057},
     language = {en},
     url = {http://archive.numdam.org/articles/10.1051/ita:2003001/}
}

TY  - JOUR
AU  - Cortier, Véronique
TI  - About the decision of reachability for register machines
JO  - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
PY  - 2002
SP  - 341
EP  - 358
VL  - 36
IS  - 4
PB  - EDP-Sciences
UR  - http://archive.numdam.org/articles/10.1051/ita:2003001/
DO  - 10.1051/ita:2003001
LA  - en
ID  - ITA_2002__36_4_341_0
ER  -

%0 Journal Article
%A Cortier, Véronique
%T About the decision of reachability for register machines
%J RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
%D 2002
%P 341-358
%V 36
%N 4
%I EDP-Sciences
%U http://archive.numdam.org/articles/10.1051/ita:2003001/
%R 10.1051/ita:2003001
%G en
%F 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://archive.numdam.org/articles/10.1051/ita:2003001/

Bibliographie
Cité par

[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

[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

[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 | MR

[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 | Zbl

[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

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

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

Cité par Sources :