On Efficient Models for Model Checking Message-Passing Distributed Protocols

The complexity of distributed algorithms, such as state machine replication, motivates the use of formal methods to assist correctness verification. The design of the formal model of an algorithm directly affects the efficiency of the analysis. Therefore, it is desirable that this model does not add "Unnecessary" complexity to the analysis. In this paper, the authors consider a general Message-Passing (MP) model of distributed algorithms and compare different ways of modeling the message traffic. They prove that the different MP models are equivalent with respect to the common properties of distributed algorithms. Therefore, one can select the model which is best suited for the applied verification technique.