Layered reasoning for randomized distributed algorithms

DOI10.1007/S00165-012-0231-XzbMATH Open1259.68114DBLPjournals/fac/SwaminathanKO12OpenAlexW1999872864WikidataQ57801088 ScholiaQ57801088MaRDI QIDQ1941864FDOQ1941864

Authors: Mani Swaminathan, Ernst-Rüdiger Olderog, Joost-Pieter Katoen 

Publication date: 22 March 2013

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-012-0231-x

Recommendations

• RDA: a Coq library to reason about randomised distributed algorithms in the message passing model
• Validation of Stochastic Systems
• scientific article; zbMATH DE number 1786476
• scientific article; zbMATH DE number 2006656
• Verification of the randomized consensus algorithm of Aspnes and Herlihy: a case study

zbMATH Keywords

probabilistic automatacommunication closednesslayered composition and separationpartial order equivalencerandomizedmutual exclusion

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Randomized algorithms (68W20) Distributed algorithms (68W15)

Cites Work

• Analyzing security protocols using time-bounded task-PIOAs
• Title not available (Why is that?)
• Title not available (Why is that?)
• N-process mutual exclusion with bounded waiting by 4. log//2N-valued shared variable
• A layered analysis of consensus
• Decomposition of distributed programs into communication-closed layers
• Using probabilistic Kleene algebra pKA for protocol verification
• A principle for sequential reasoning about distributed algorithms
• Layered composition for timed automata
• Randomized mutual exclusion algorithms revisited
• Confluence Reduction for Probabilistic Systems
• Title not available (Why is that?)
• Tight bounds for asynchronous randomized consensus
• A linear process-algebraic format with data for probabilistic automata
• Proving probabilistic correctness statements: the case of Rabin's algorithm for mutual exclusion
• Title not available (Why is that?)
• From sequential layers to distributed processes
• Title not available (Why is that?)

Cited In (2)

• Title not available (Why is that?)
• Structural transformations for data-enriched real-time systems

Uses Software

• PRISM

This page was built for publication: Layered reasoning for randomized distributed algorithms

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