论文标题
二元格2.0：通过阶段图解释人口协议的正确性
Peregrine 2.0: Explaining Correctness of Population Protocols through Stage Graphs
论文作者
论文摘要
我们提出了一种新版本的Peregrine，这是[Blondin等，Cav'2018]中引入的人群协议的分析和参数化验证的工具。人口协议是一种计算模型，由分布式计算社区深入研究，其中移动匿名代理随机互动以执行任务。 Peregrine 2.0具有基于舞台图的构造的新型验证引擎。舞台图是[Blondin等，Cav'2020]中引入的证明证书，通常是简洁的，可以独立检查。此外，与二元格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.
