Convergence Verification of Asynchronous Iterations

This paper describes a novel approach to convergence verification of asynchronous iterations in addition to reachability analysis of them. Asynchronous iterations are computation schemes capable of capturing all possible behaviors of distributed systems employing connectionless communication protocols such as UDP/IP. The robustness of these systems against uncertainty in packet delivery can be assured by proving their convergence. We construct some theorems on the basis of fixpoint computations to derive a method for convergence verification, and implement it in trial programs using binary decision diagrams. Theoretical analysis reveals its effectiveness in reducing memory usage, and experimental results support its extreme advantage in execution times. They suggest the possibility of practical use of this method.