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
topHow 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 ?
topYou must be logged in to post comments.
To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.