%0 Conference Paper %1 10.1007/978-3-030-67067-2_11 %A Bertrand, Nathalie %A Lazić, Marijana %A Widder, Josef %B Verification, Model Checking, and Abstract Interpretation %D 2021 %E Henglein, Fritz %E Shoham, Sharon %E Vizel, Yakir %I Springer International Publishing %K conference %P 219--239 %R 10.1007/978-3-030-67067-2_11 %T A Reduction Theorem for Randomized Distributed Algorithms Under Weak Adversaries %U https://link.springer.com/chapter/10.1007%2F978-3-030-67067-2_11 %X Weak adversaries are a way to model the uncertainty due to asynchrony in randomized distributed algorithms. They are a standard notion in correctness proofs for distributed algorithms, and express the property that the adversary (scheduler), which has to decide which messages to deliver to which process, has no means of inferring the outcome of random choices, and the content of the messages.In this paper, we introduce a model for randomized distributed algorithms that allows us to formalize the notion of weak adversaries. It applies to randomized distributed algorithms that proceed in rounds and are tolerant to process failures. For this wide class of algorithms, we prove that for verification purposes, the class of weak adversaries can be restricted to simple ones, so-called round-rigid adversaries, that keep the processes tightly synchronized. As recently a verification method for round-rigid adversaries has been introduced, our new reduction theorem paves the way to the parameterized verification of randomized distributed algorithms under the more realistic weak adversaries. %@ 978-3-030-67067-2

@inproceedings{10.1007/978-3-030-67067-2_11, abstract = {Weak adversaries are a way to model the uncertainty due to asynchrony in randomized distributed algorithms. They are a standard notion in correctness proofs for distributed algorithms, and express the property that the adversary (scheduler), which has to decide which messages to deliver to which process, has no means of inferring the outcome of random choices, and the content of the messages.In this paper, we introduce a model for randomized distributed algorithms that allows us to formalize the notion of weak adversaries. It applies to randomized distributed algorithms that proceed in rounds and are tolerant to process failures. For this wide class of algorithms, we prove that for verification purposes, the class of weak adversaries can be restricted to simple ones, so-called round-rigid adversaries, that keep the processes tightly synchronized. As recently a verification method for round-rigid adversaries has been introduced, our new reduction theorem paves the way to the parameterized verification of randomized distributed algorithms under the more realistic weak adversaries.}, added-at = {2021-01-18T13:18:29.000+0100}, author = {Bertrand, Nathalie and Lazi{\'{c}}, Marijana and Widder, Josef}, biburl = {https://www.bibsonomy.org/bibtex/20f156cadf836bd673a22a61aa2059fd3/paves}, booktitle = {Verification, Model Checking, and Abstract Interpretation}, doi = {10.1007/978-3-030-67067-2_11}, editor = {Henglein, Fritz and Shoham, Sharon and Vizel, Yakir}, interhash = {6ad1b5f62c9e2512fe89c29be4df68d3}, intrahash = {0f156cadf836bd673a22a61aa2059fd3}, isbn = {978-3-030-67067-2}, keywords = {conference}, pages = {219--239}, publisher = {Springer International Publishing}, timestamp = {2023-09-24T19:42:04.000+0200}, title = {A Reduction Theorem for Randomized Distributed Algorithms Under Weak Adversaries}, url = {https://link.springer.com/chapter/10.1007%2F978-3-030-67067-2_11}, year = 2021 }