An Automatic Real-Time Analysis of the Time to Reach Consensus

Consensus is one of the most fundamental problems in fault-tolerant distributed computing. This paper proposes a mechanical method for analyzing the condition that allows one to solve consensus. Specifically, we model check a distributed algorithm that implements a communication predicate, which is an alternative system abstraction to failure detectors. This model checking problem is challenging because it involves both continuous time and unbounded integers. We solve the problem by reducing it to the satisfiability problem of linear arithmetic constraints over real and integer variables. The proposed method can be used to determine the length of a synchronous period required for implementing a communication predicate for solving consensus.