关于自动稳定人口协议的验证

人口协议模型已经成为描述移动自组织网络的一种优雅的计算范例,该模型由许多相互交互以执行计算的移动节点组成。 节点的交互受公平性约束。 填充协议的一项基本属性是,所有节点最终都必须收敛到正确的输出值(或配置)。 在本文中,我们旨在在Spin模型检查器中自动验证用于领导者选举和令牌流通的自我稳定种群协议。 我们报告我们的验证结果,并讨论在Spin中建模强公平性约束的问题。