arXiv:2611.07919 · v1

Modular Parameterized Model Checking of Threshold-Based Distributed Algorithms

首次提交 2026-11-05 20:29

版本更新 2026-11-05 20:29

雷达观测 2026-11-06 11:06

摘要

We present a novel approach for model checking fault-tolerant distributed algorithms: instead of building large, monolithic algorithm models, we propose a modular approach where the user decomposes the algorithm into modules, verifies them individually, and replaces them with a synchronous abstraction. To enable our technique, we introduce a new system model that combines aspects of threshold automata and global synchronization protocols. We investigate the expressiveness of our new model, and present a (bounded) model checking procedure as well as a method for checking the correctness of the abstraction step. We implemented the technique and report on promising experimental results on a case study

作者备注：18 pages + 6 pages acknowledgements & references + 13 pages appendix = 37 pages; 9 Figures + 4 Algorithms