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

DOI10.1007/PL00008917zbMath1448.68156MaRDI QIDQ5137903

Roberto Segala, Anna Pogosyants, Nancy A. Lynch

Publication date: 3 December 2020

Published in: Distributed Computing (Search for Journal in Brave)

zbMATH Keywords

verificationperformance analysisprobabilistic automatarandomized consensus

Mathematics Subject Classification ID

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

Related Items

What is decidable about partially observable Markov decision processes with \(\omega\)-regular objectives, Switched PIOA: parallel composition via distributed scheduling, Compositional probabilistic verification through multi-objective model checking, Simple stochastic games with almost-sure energy-parity objectives are in NP and conp, The complexity of synchronizing Markov decision processes, Task-structured probabilistic I/O automata, 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, CEGAR for compositional analysis of qualitative properties in Markov decision processes, POMDPs under probabilistic semantics, Qualitative analysis of concurrent mean-payoff games

Cites Work

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