Dynamic asynchronous iterations.

• Mathematical model of "dynamic" asynchronous iterations. • Both the function being iterated and the participants change over time. • Formal definition of what it means for such processes to behave "correctly". • Derives sufficient conditions for correctness. • Formally verified in the proof assistant Agda, library is publicly available. Many problems can be solved by iteration by multiple participants (processors, servers, routers etc.). Previous mathematical models for such asynchronous iterations assume a single function being iterated by a fixed set of participants. We will call such iterations static since the system's configuration does not change. However in several real-world examples, such as inter-domain routing, both the function being iterated and the set of participants change frequently while the system continues to function. In this paper we extend Üresin and Dubois's work on static iterations to develop a model for this class of dynamic or always on asynchronous iterations. We explore what it means for such an iteration to be implemented correctly, and then prove two different conditions on the set of iterated functions that guarantee the full asynchronous iteration satisfies this new definition of correctness. These results have been formalised in Agda and the resulting library is publicly available. [ABSTRACT FROM AUTHOR]