For the most recent entries see the Petri Nets Newsletter.

Verification of the Randomized Consensu Algorithm of Aspnes and Herlihy: a Case Study.

Pogosyants, A.; Segala, R.; Lynch, N.

In: Mavronicolas, M.; Tsigas, Ph.: Lecture Notes in Computer Science, Vol. 1320: Distributed Algorithms, Proc. of 11th International Workshop, WDAG'97, Saarbrücken, Germany, pages 22-36. Springer, September 1997.

Abstract: The Probabilistic I/O Automaton model is used as the basis for a formal presentation and proof of the randomized consensus algorithm of Aspnes and Herlihy. The algorithm is highly nontrivial and guarantees termination within expected polynomial time. The task of carrying out this proof has led us to develop several general proof techniques for probabilistic I/O automata. These include ways to combine expectations for different complexity measures, to compose expected complexity properties, to convert probabilistic claims to deterministic claims, to use abstraction mappings to prove probabilistic properties, and to apply random walk theory in a distributed computational setting.


Do you need a refined search? Try our search engine which allows complex field-based queries.

Back to the Petri Nets Bibliography