Threshold automata are a computational model that has proven to be versatile in modeling threshold-based distributed algorithms and enabling their completely automatic parameterized verification. We present novel techniques for the verification of threshold automata, based on well-structured transition systems, that allow us to extend the expressiveness of both the computational model and the specifications that can be verified. In particular, we extend the model to allow decrements and resets of shared variables, possibly on cycles, and the specifications to general coverability. While these extensions of the model in general lead to undecidability, our algorithms provide a semi-decision procedure. We demonstrate the benefit of our extensions by showing that we can model complex round-based algorithms such as the phase king consensus algorithm and the Red Belly Blockchain protocol (published in 2019), and verify them fully automatically for the first time.

翻译：阈值自动机是一种计算模型，已证明其在建模基于阈值的分布式算法及实现其完全自动化参数化验证方面具有广泛适用性。我们提出了基于良结构迁移系统的阈值自动机验证新技术，这些技术扩展了计算模型与可验证规约的表达能力。具体而言，我们扩展了模型以支持共享变量的递减与重置操作（允许在循环中执行），并将规约扩展至广义可覆盖性。虽然这些模型扩展通常会导致不可判定性，但我们的算法提供了半判定过程。我们通过建模复杂轮次算法（如phase king共识算法与2019年发布的Red Belly区块链协议）并首次实现其全自动验证，展示了所提扩展的实际价值。