On Convergence of Concurrent Systems under Regular Interactions

Convergence is often the key liveness property for distributed systems that interact with physical processes. Techniques for proving convergence (asymptotic stability) have been extensively studied by control theorists. In particular, for the asynchronous model of computation Tsitsiklis [8] provides a set of necessary and sufficient conditions for proving stability and convergence under the assumption that each asynchronous operator (state transition function) is applied infinitely often. This paper generalize these results to obtain necessary and sufficient conditions for systems where the infinite sequence of operators is a member of an arbitrary omega regular language. This enables us to apply our theory to distributed systems with changing communication topology, node failures and joins. We illustrate an application of the new set of conditions in verifying the convergence of a simple (continuous) consensus protocol.

• Type: Journal
• Year: 2009
• Where: CONCUR
• Authors: Pavithra Prabhakar, Sayan Mitra, Mahesh Viswanathan
• Keywords: CONCUR 2009, Convergence, Distributed And Parallel Computing, Key Liveness Property, Sufficient Conditions