Parameterized Distributed Synthesis of Fault-Tolerance Using Counter Abstraction

In this paper, we propose an automated technique for synthesizing fault-tolerant distributed protocols from their fault-intolerant version, where the number of processes is parameterized. A fault-tolerant protocol is one that ensures constant
satisfaction of safety and liveness specifications even in the presence of faults. Although the parametrized synthesis problem is undecidable in general, we could propose a sound algorithm for this challenging problem. Our synthesis algorithm utilizes counter abstraction to construct a finite representation of the state space. Then, it performs fixpoint calculations to compute and exclude states that violate the safety/liveness specifications in the presence of faults. We demonstrate the effectiveness of our algorithm by synthesizing fault-tolerant distributed protocols for well-known problems, such as reliable broadcast and a simplified version of Byzantine agreement in a matter of seconds.