About Fast and TReX Accelerations

AbstractFast and TReX tools are designed to analyse systems with infinite state spaces. They both implement algorithms computing the set of reachable states of such systems. Since the state space may be infinite, acceleration techniques are used. In this paper, we study the differences between Fast and TReX acceleration techniques and show that although Fast remains in Presburger logics while accelerating, TReX can produce 1st order arithmetical formulas even when accelerating functions