Verification of the randomized consensus algorithm of Aspnes and Herlihy: a case study

DOI10.1007/PL00008917MaRDI QIDQ5137903zbMATH OpenFDO

Authors Anna Pogosyants, Roberto Segala, Nancy Lynch

Publication date 3 December 2020

Published in Distributed Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/PL00008917

zbMATH Keywords

performance analysisprobabilistic automatarandomized consensusverification

Mathematics Subject Classification ID

Distributed systems (68M14) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Randomized algorithms (68W20)

Recommendations

• scientific article; zbMATH DE number 1796134
• Randomized Consensus in Expected O(N\log ^2 N) Operations Per Processor
• The correctness proof of Ben-Or's randomized consensus algorithm
• scientific article; zbMATH DE number 1786476
• Lower bounds for randomized consensus under a weak adversary

Cites work

• Concurrent reading and writing
• Efficient asynchronous consensus with the weak adversary scheduler
• Fast randomized consensus using shared memory
• Finite state Markovian decision processes
• Formal verification of timed properties of randomized distributed algorithms
• Forward and backward simulations. I. Untimed Systems
• scientific article; zbMATH DE number 996442 (Why is no real title available?)
• scientific article; zbMATH DE number 2102783 (Why is no real title available?)
• scientific article; zbMATH DE number 3059214 (Why is no real title available?)
• Impossibility of distributed consensus with one faulty process
• Liveness in timed and untimed systems
• Model checking of probabilistic and nondeterministic systems
• Polylog randomized wait-free consensus
• Probabilistic automata
• Proving time bounds for randomized distributed algorithms
• Randomized Consensus in Expected O(N\log ^2 N) Operations Per Processor
• Termination of Probabilistic Concurrent Program
• Time- and Space-Efficient Randomized Consensus
• Time-Lapse Snapshots
• Verification of multiprocess probabilistic protocols

Cited in

(16)

• The complexity of synchronizing Markov decision processes
• Task-structured probabilistic I/O automata
• Layered reasoning for randomized distributed algorithms
• Simple stochastic games with almost-sure energy-parity objectives are in NP and conp
• Symbolic algorithms for qualitative analysis of Markov decision processes with Büchi objectives
• Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives
• POMDPs under probabilistic semantics
• Qualitative analysis of concurrent mean-payoff games
• What is decidable about partially observable Markov decision processes with \(\omega\)-regular objectives
• Compositional probabilistic verification through multi-objective model checking
• scientific article; zbMATH DE number 1786476 (Why is no real title available?)
• scientific article; zbMATH DE number 1796134 (Why is no real title available?)
• Proving probabilistic correctness statements: the case of Rabin's algorithm for mutual exclusion
• Verification of randomized consensus algorithms under round-rigid adversaries
• CEGAR for compositional analysis of qualitative properties in Markov decision processes
• Switched PIOA: parallel composition via distributed scheduling

This page was built for publication: Verification of the randomized consensus algorithm of Aspnes and Herlihy: a case study

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5137903)