Peregrine 2.0：通过阶段图解释种群协议的正确性
Peregrine 2.0: Explaining Correctness of Population Protocols through Stage Graphs
摘要：
我们提出了一个新版本的Peregrine，用于分析和参数化验证人口协议的工具[Blondin et al.，CAV'2018]。群体协议是一种计算模型，分布式计算社区对其进行了深入的研究，其中移动匿名代理随机交互以执行任务。Peregrine 2.0提供了一个基于阶段图构造的新型验证引擎。阶段图是证明证书，在[Blondin等人，CAV'2020]，其通常简洁并且可以独立检查。此外，与Peregrine 1.0的技术不同，阶段图方法可以验证执行永不终止的协议，这类协议包括最近的快速多数协议。Peregrine 2.0还具有一个新颖的证明可视化组件，允许用户交互式地探索为给定协议生成的阶段图。
英文摘要：
We present a new version of Peregrine, the tool for the analysis and parameterized verification of population protocols introduced in [Blondin et al., CAV'2018]. Population protocols are a model of computation, intensely studied by the distributed computing community, in which mobile anonymous agents interact stochastically to perform a task. Peregrine 2.0 features a novel verification engine based on the construction of stage graphs. Stage graphs are proof certificates, introduced in [Blondin et al., CAV'2020], that are typically succinct and can be independently checked. Moreover, unlike the techniques of Peregrine 1.0, the stage graph methodology can verify protocols whose executions never terminate, a class including recent fast majority protocols. Peregrine 2.0 also features a novel proof visualization component that allows the user to interactively explore the stage graph generated for a given protocol.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
