CONVERGENCE OF ITERATION SYSTEMS

An iteration system is a set of assignment statements whose computatio n proceeds in steps: at each step, an arbitrary subset of the statemen ts is executed in parallel. The set of statements thus executed may di ffer at each step; however, it is required that each statement is exec uted infinitely often along the computation. The convergence of such s ystems (to a fixed point) is typically verified by showing that the va lue of a given variant function is decreased by each step that causes a state change. Such a proof requires an exponential number of cases ( in the number of assignment statements) to be considered. In this pape r, we present alternative methods for verifying the convergence of ite ration systems. In most of these methods, upto a linear number of case s need to be considered.