# About the decision of reachability for register machines

RAIRO - Theoretical Informatics and Applications (2010)

- Volume: 36, Issue: 4, page 341-358
- ISSN: 0988-3754

## Access Full Article

top## Abstract

top## How to cite

topCortier, Véronique. "About the decision of reachability for register machines." RAIRO - Theoretical Informatics and Applications 36.4 (2010): 341-358. <http://eudml.org/doc/92706>.

@article{Cortier2010,

abstract = {
We study the decidability of the following problem: given p affine
functions ƒ1,...,ƒp over $\mathbb\{N\}^k$ and two vectors $v_1, v_2\in\mathbb\{N\}^k$,
is v2 reachable from v1 by successive iterations of ƒ1,...,ƒp
(in this given order)?
We show that this question is decidable for p = 1, 2 and undecidable for
some fixed p.
},

author = {Cortier, Véronique},

journal = {RAIRO - Theoretical Informatics and Applications},

keywords = {Verification; infinite state systems.; verification; infinite state systems; decidability},

language = {eng},

month = {3},

number = {4},

pages = {341-358},

publisher = {EDP Sciences},

title = {About the decision of reachability for register machines},

url = {http://eudml.org/doc/92706},

volume = {36},

year = {2010},

}

TY - JOUR

AU - Cortier, Véronique

TI - About the decision of reachability for register machines

JO - RAIRO - Theoretical Informatics and Applications

DA - 2010/3//

PB - EDP Sciences

VL - 36

IS - 4

SP - 341

EP - 358

AB -
We study the decidability of the following problem: given p affine
functions ƒ1,...,ƒp over $\mathbb{N}^k$ and two vectors $v_1, v_2\in\mathbb{N}^k$,
is v2 reachable from v1 by successive iterations of ƒ1,...,ƒp
(in this given order)?
We show that this question is decidable for p = 1, 2 and undecidable for
some fixed p.

LA - eng

KW - Verification; infinite state systems.; verification; infinite state systems; decidability

UR - http://eudml.org/doc/92706

ER -

## References

top- 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.
- B. Boigelot, Symbolic Methods for Exploring Infinite Sate Spaces, Ph.D. Thesis. Université de Liège (1998) 225.
- 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.
- V. Cortier, Vérification de systèmes à compteurs (in French), Master's Thesis. Université Paris 7 (1999) URIhttp://www.lsv.ens-cachan.fr/cortier/memoire_dea.ps
- L.E. Dickson, Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors. Amer. J. Math.35 (1913) 413-422.
- 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.
- A. Finkel, P. McKenzie and C. Picaronny, A well-structured framework for analysing Petri nets extensions. Technical Report, Research Report LSV-99-2 (1999) URIhttp://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/rr-lsv-1999-2.rr.ps
- M.Yu. Matijacevitch, M. David and J. Robinson, Hilbert's Tenth Problem, Chapter 3 (1976).
- C. Rorres and H. Anton, Applications of Linear Algebra, Chapters 9 and 13 (1979).

## NotesEmbed ?

topTo embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.