Automated Verification of Multi-Party Agreements and Scheduling of Sending Messages in Distributed Ledger Systems

Multi-party agreements are used in distributed ledger systems and blockchain networks to reach an agreement on changes in the system. When one of the network participants proposes a transaction to be recorded, it should be first confirmed by certain network participants. A multi-party agreement or consensus determines who exactly these participants are. Based on the historical data set, one can calculate the transaction confirmation probability for each of the participants. In this work, a method of statistical model checking is proposed to determine the probability that the consensus is reached. Sending confirmation requests may require extra costs. In addition to the stated probability, the mathematical expectation of the number of messages received before reaching a consensus is calculated. A consensus model or several consensus models are given in the form of a Markov chain with various message sending strategies. Based on the construction algorithms for the model and specification, a tool that analyzes consensus and sends confirmation messages is developed.