About the decision of reachability for register machines
Laboratoire Spécification et Vérification,
École Normale Supérieure de Cachan, CNRS,
61 avenue du Président Wilson, 94230 Cachan, France;
Accepted: October 2002
We study the decidability of the following problem: given p affine functions ƒ1,...,ƒp over and two vectors , 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.
Mathematics Subject Classification: 68Q60
Key words: Verification / infinite state systems.
© EDP Sciences, 2002