Gossip protocols are an important class of network algorithms that rely on local connectivity to propagate information globally. The model described here comprises 4 node components and a scheduler component. The scheduler selects nondeterministically the order in which nodes execute the protocol. The node randomly selects with which peer they are connecting. A PLASMA Lab project that contains the example is available here.
We use the smart estimating algorithm to estimate the minimum and maximum probabilities that the maximum path length in the network is less than 4. We test this property for a range of times (T), such that the property that is checked is F<=#T max_path_length < 4.
We plot below the results obtain with 100’000 simulations budget, epsilon and delta equal to 0.01.
We then use the reward estimation algorithm. We first check a reachability reward to estimate the expected minimum and maximum number of rounds necessary for the network to become connected to be 1.486 and 4.5. The correct values are 1.5 and 4.5.
Finally we use an instantaneous reward property to estimate the minimum and maximum path length at different time steps. The algorithm also generate the average estimates of the initial candidate set of schedulers. This average corresponds to the expected reward using the uniform probabilistic scheduler. We plot the results in the figure below. The solid lines give the values calculated using numerical algorithms. The true value for the uniform probabilistic scheduler is calculated numerically by treating the MDP as a DTMC. We see that the estimates of maximum and minimum expected reward are accurate up to about 75 time steps, but less so above this value. The estimates are nevertheless guaranteed not to exceed the true values by more than a factor of 
