Learning Broadcast Protocols

The problem of learning a computational model from examples has been receiving growing attention. Models of distributed systems are particularly challenging since they encompass an added succinctness. While positive results for learning some models of distributed systems have been obtained, so far the considered models assume a fixed number of processes interact. In this work we look for the first time (to the best of our knowledge) at the problem of learning a distributed system with an arbitrary number of processes, assuming only that there exists a cutoff. Specifically, we consider fine broadcast protocols, these are broadcast protocols (BPs) with a finite cutoff and no hidden states. We provide a learning algorithm that given a sample consistent with a fine BP, can infer a correct BP, with the help of an SMT solver. Moreover we show that the class of fine BPs is teachable, meaning that we can associate a finite set of words $\mathcal{S}_B$ with each BP $B$ in the class (a so-called characteristic set) so that the provided learning algorithm can correctly infer a correct BP from any consistent sample subsuming $\mathcal{S}_B$. On the negative size we show that (a) characteristic sets of exponential size are unavoidable, (b) the consistency problem for fine BPs is NP hard, and (c) fine BPs are not polynomially predictable.