2026-08-25T22:09:00Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:27351 2026-08-24T14:08:30Z ddc:004 open_access

Parameterized Verification of Asynchronous Round-Based Distributed Algorithms via Reduction to Finite-Counter Systems Bertrand, Nathalie Ghorpade, Pranav Rubin, Sasha parametrized verification asynchronous round-based distributed algorithms finite-counter systems LTL model checking Traditional model-checking techniques typically verify distributed algorithms only for a fixed number of finite-state processes. Parameterized model checking generalizes this to any number of processes, while still typically assuming that each process is finite-state. In this work, we consider asynchronous round-based distributed algorithms in which each process is infinite-state since it can execute for an infinite number of rounds. We show that the parameterized verification problem for asynchronous round-based distributed algorithms is undecidable, already for simple specifications. Nevertheless, as our main contribution, we provide a reduction to LTL model checking over finite-counter systems and prove that it is sound and complete. This enables the use of off-the-shelf, mature symbolic model checkers for finite-counter systems. We demonstrate the practical applicability of this reduction by verifying safety and liveness properties of several asynchronous round-based consensus and leader-election algorithms using the nuXmv model checker. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Nathalie Bertrand and Pranav Ghorpade and Sasha Rubin 2026 Is Part Of LIPIcs, Volume 391, 37th International Conference on Concurrency Theory (CONCUR 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2026.20 urn:nbn:de:0030-drops-273511 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.20 eng https://creativecommons.org/licenses/by/4.0/legalcode