On iterating linear transformations over recognizable sets of integers
it has been known for a long time that the sets of integer vectors that are recognizable by finite-state automata are those that can be defined in an extension of Presburger arithmetic. In this paper, we address the problem of deciding whether the closure of a linear transformation preserves the recognizable nature of sets of integer vectors. We solve this problem by introducing an original extension of the concept of recognizability to sets of vectors with complex components. This generalization allows to obtain a simple necessary and sufficient condition over linear transformations, in terms of the eigenvalues of the transformation matrix. We then show that these eigenvalues do not need to be computed explicitly in order to evaluate the condition, and we give a full decision procedure based on simple integer arithmetic. The proof of this result is constructive, and can be turned into an algorithm for applying the closure of a linear transformation that satisfies the condition to a finite-state representation of a set. Finally, we show that the necessary and sufficient condition that we have obtained can straightforwardly be turned into a sufficient condition for linear transformations with linear guards. (C) 2003 Elsevier B.V . All rights reserved.
iterations recognizable sets of integers automata presburger arithmetic