RAIRO - Theoretical Informatics and Applications

Research Article

About the decision of reachability for register machines

Véronique Cortier

Laboratoire Spécification et Vérification, École Normale Supérieure de Cachan, CNRS, 61 avenue du Président Wilson, 94230 Cachan, France; cortier@lsv.ens-cachan.fr.

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 v 2 reachable from v 1 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.

(Received May 2001)

(Accepted October 2002)

(Online publication February 15 2003)

Key Words:

  • Verification;
  • infinite state systems.

Mathematics Subject Classification:

  • 68Q60
Metrics