Skip to content

feat(FLP): develop the theory of pseudo-consensus algorithms that can tolerate up to 1 fault - #755

Open
ctchou wants to merge 3 commits into
leanprover:mainfrom
ctchou:flp-pseudo-1
Open

feat(FLP): develop the theory of pseudo-consensus algorithms that can tolerate up to 1 fault#755
ctchou wants to merge 3 commits into
leanprover:mainfrom
ctchou:flp-pseudo-1

Conversation

@ctchou

@ctchou ctchou commented Jul 29, 2026

Copy link
Copy Markdown
Collaborator

This PR develops a theory of pseudo-consensus algorithms that can tolerate up to 1 fault, which is the core of Völzer's argument. The central notion is "non-uniformity": a state s is non-uniform iff for each boolean value b, there exists a process p such that there is an execution of the algorithm from s that ends up deciding on b without the participation of p. Then any algorithm that can tolerate up to 1 fault is proved to have two properties:
(1) nonUniform_inp, which says that there must an initial non-uniform state.
(2) nonUniform_step, which will be shown in the next PR to guarantee that any execution ending in a non-uniform state can be extended to a longer execution ending in a non-uniform state.

Comment thread Cslib/Computability/Distributed/FLP/OnePseudoConsensus.lean Outdated
Comment thread Cslib/Computability/Distributed/FLP/OnePseudoConsensus.lean
Comment thread Cslib/Computability/Distributed/FLP/OnePseudoConsensus.lean
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants