Affordable Access

About the decision of reachability for register machines

Publication Date
  • Mathematics


ita0220.dvi Theoretical Informatics and Applications Theoret. Informatics Appl. 36 (2002) 341–358 DOI: 10.1051/ita:2003001 ABOUT THE DECISION OF REACHABILITY FOR REGISTER MACHINES Ve´ronique Cortier1 Abstract. We study the decidability of the following problem: given p affine functions f1, . . . , fp over N k and two vectors v1, v2 ∈ Nk , is v2 reachable from v1 by successive iterations of f1, . . . , fp (in this given order)? We show that this question is decidable for p = 1, 2 and unde- cidable for some fixed p. Mathematics Subject Classification. 68Q60. Introduction Reachability is a fundamental question for computation models: a typical safety property of a reactive system is the unreachability of some catastrophic state. Reachability is straightforwardly decidable (in a time linear in the number of states) for �nite-state systems. For other (in�nite-state) computation models, it is most of the time undecidable. In this paper, we study the border between decidability and undecidability for a particular computation model: con�gurations are vectors of non-negative integers. Each move from a con�guration to its successor is given by an a�ne function f(X) = AX + B where A is a matrix of non-negative integers and B is a vector of integers. Such a�ne functions are used to model the evolution of dynamical systems like the age repartition of trees of a forestry development or the human population growth (see [9]): the initial vector represents the initial repartition and the a�ne function describe the evolution of this repartition during a year. They can also be used to compute limit trajectories (see [1]). Keywords and phrases: Verification, infinite state systems. 1 Laboratoire Spe´cification et Ve´rification, E´cole Normale Supe´rieure de Cachan, CNRS, 61 avenue du Pre´sident Wilson, 94230 Cachan, France; e-mail: [email protected] c© EDP Sciences 2003 342 V. CORTIER Petri nets with transfer are a particular case of this model (components of A are 0 or 1), hence re

There are no comments yet on this publication. Be the first to share your thoughts.