2026-07-21T23:35:07Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:25202 2026-03-19T12:59:33Z ddc:004 open_access

How Exhaustive Does an Extension-Based Proof Need to Be? Ellen, Faith Liu, Shihao Zhu, Leqi Gafni, Eli Gelashvili, Rati Extension-based proof set agreement valency argument zero-one exclusion The class of extension-based proofs encompasses traditional valency arguments. It has been shown that they are insufficient to establish the impossibility of (n-1)-set agreement among n ≥ 3 processes in an asynchronous system with crash failures. We generalize this definition to k-exhaustive extension-based proofs, in which a prover can learn the maximum length of all executions involving a set of at most k processes from a specified configuration (which may be infinite). An upper bound on the length of these executions enables the prover to determine the outputs of all these executions. When k = n, this enables the prover to perform an exhaustive search of all reachable configurations, so it knows everything about the protocol. On the other hand, extension based proofs are as powerful as 1-exhaustive extension-based proofs. For any task with no deterministic, wait-free solution among n ≥ 2 processes, we show that there is an (n-1)-exhaustive extension-based proof of its impossibility. This is done using a new characterization of such tasks. In contrast, we prove that for 1 ≤ k ≤ n-2, there is no k-exhaustive extension-based proof of the impossibility of (n-1)-set agreement. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Faith Ellen and Shihao Liu and Leqi Zhu and Eli Gafni and Rati Gelashvili 2026 Is Part Of LIPIcs, Volume 361, 29th International Conference on Principles of Distributed Systems (OPODIS 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.OPODIS.2025.29 urn:nbn:de:0030-drops-252020 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2025.29 eng https://creativecommons.org/licenses/by/4.0/legalcode