The gossip problem provides a simple model of information exchange in distributed systems. For the analysis and verification of gossip protocols, logics have been developed, but manual computation and case analysis can be tedious and error-prone.
Here we present GoMoChe, a special-purpose model checker for gossip. The tool can decide when protocols known from the literature such as “Learn New Secrets” are successful. GoMoChe uses a version of epistemic logic with protocol-dependent knowledge and was developed to find and verify results in previous work.
The main version models a synchronous setting where agents always know how many calls happened, but we also provide an experimental version for asynchronous settings where agents only observe their own calls.