We study the decidability of the following problem: given affine functions over and two vectors , is reachable from by successive iterations of (in this given order)? We show that this question is decidable for and undecidable for some fixed .
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/
[1] 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
, and ,[2] Symbolic Methods for Exploring Infinite Sate Spaces, Ph.D. Thesis. Université de Liège (1998) 225.
,[3] 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
and ,[4] Vérification de systèmes à compteurs (in French), Master's Thesis. Université Paris 7 (1999) http://www.lsv.ens-cachan.fr/cortier/memoire_dea.ps
,[5] Finiteness of the odd perfect and primitive abundant numbers with distinct prime factors. Amer. J. Math. 35 (1913) 413-422. | JFM | MR
,[6] Between decidability and undecidability, in Proc. ICALP 1998. Springer-Verlag, Lecture Notes in Comput. Sci. 1448 (1998) 103-115. | MR | Zbl
, and ,[7] 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
, and ,[8] Hilbert's Tenth Problem, Chapter 3 (1976). | Zbl
, and ,[9] Applications of Linear Algebra, Chapters 9 and 13 (1979). | Zbl
and ,Cité par Sources :