On Learnability of Broadcast Protocols

Summary

We study passive learning of broadcast protocols (BPs), a well-studied model of parametrized concurrent systems in which an arbitrary number of identical processes communicate via synchronized broadcasts. Prior grammatical inference results for concurrent models assumed a fixed, known number of components; these results fall short for parametrized protocols, which must be correct for any number of processes. We focus on the class of fine BPs, those with a finite cutoff and no hidden states, and establish the first grammatical inference framework for a concurrent model in the fully parametrized setting. A central obstacle is the absence of a canonical minimal representative: two non-isomorphic minimal fine BPs accepting the same language nonetheless share a tight structural correspondence. We show that a sufficiently complete sample, one that subsumes a characteristic set, forces a learner to recover this correspondence exactly. Building on this, we present a passive learning algorithm that encodes BP-consistency as a constraint system in the theory of equality with uninterpreted functions (EUF), decidable and solvable by standard SMT solvers. Furthermore, when the sample is sufficiently complete, the algorithm returns a minimal language-equivalent fine BP. We complement these results with three hardness results: consistency checking is NP-complete, characteristic sets may be exponentially large, and fine BPs are not polynomially predictable under standard cryptographic assumptions. Taken together, these results give a comprehensive learnability picture for a class of concurrent models that directly supports parametrized verification.