RAIRO - Theoretical Informatics and Applications

Table of Contents - October 2002 - Volume 36, Issue 04  

Research Article

About the decision of reachability for register machines

Cortier, Véronique

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