Truncating and Shifting Weights for Max-Plus Automata

In this paper, for any real number λ, we transform the complete max-plus semiring R∞ into a commutative, complete, additively idempotent semiring R∞λ, called the lower λ-truncation of R∞. It is obtained by removing from R∞ all real numbers smaller than λ, inheriting the addition operation, shifting the original products by −λ, and appropriately modifying the residuum operation. The purpose of lower truncations is to transfer the iterative procedures for computing the greatest presimulations and prebisimulations between max-plus automata, in cases where they cannot be completed in a finite number of iterations over R∞, to R∞λ, where they could terminate in a finite number of iterations. For instance, we prove that this necessarily happens when working with max-plus automata with integer weights. We also show how presimulations and prebisimulations computed over R∞λ can be transformed into presimulations and prebisimulations between the original automata over R∞. Although they do not play a significant role from the standpoint of computing presimulations and prebisimulations, for theoretical reasons we also introduce two types of upper truncations of the complete max-plus semiring R∞.