Insights into Learning Broadcast Protocols
摘要
Broadcast protocols (BPs) are a formal model of distributed systems with an unbounded number of processes communicating through broadcasts. We study the problem of passively learning BPs from execution traces, focusing on the class of fine BPs which does not have hidden states and admits a cutoff. We present a passive learning algorithm with a constraint-based approach that guarantees consistency with the sample, and returns a minimal equivalent BP if the sample is sufficiently complete (i.e., subsumes a characteristic set). Furthermore, we describe LeoParDS, the first tool that implements these techniques, supporting the practical inference of fine BPs, as well as tasks that include sample generation and approximate equivalence checking. This work was previously published at AAAI’24 [8] and later implemented at ATVA’24 [12]. We summarize its main results here to foster discussion within the cybersecurity and verification community. This short paper is intended as a concise overview for readers unfamiliar with both prior publications.