2026-08-07T05:25:07Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:16454 2024-03-06T10:57:31Z ddc:004 open_access

Parameterized Safety Verification of Round-Based Shared-Memory Systems Bertrand, Nathalie Markey, Nicolas Sankur, Ocan Waldburger, Nicolas Verification Parameterized models Distributed algorithms We consider the parameterized verification problem for distributed algorithms where the goal is to develop techniques to prove the correctness of a given algorithm regardless of the number of participating processes. Motivated by an asynchronous binary consensus algorithm [James Aspnes, 2002], we consider round-based distributed algorithms communicating with shared memory. A particular challenge in these systems is that 1) the number of processes is unbounded, and, more importantly, 2) there is a fresh set of registers at each round. A verification algorithm thus needs to manage both sources of infinity. In this setting, we prove that the safety verification problem, which consists in deciding whether all possible executions avoid a given error state, is PSPACE-complete. For negative instances of the safety verification problem, we also provide exponential lower and upper bounds on the minimal number of processes needed for an error execution and on the minimal round on which the error state can be covered. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Nathalie Bertrand and Nicolas Markey and Ocan Sankur and Nicolas Waldburger 2022 Is Part Of LIPIcs, Volume 229, 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ICALP.2022.113 urn:nbn:de:0030-drops-164541 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2022.113 eng https://creativecommons.org/licenses/by/4.0/legalcode