Layered reasoning for randomized distributed algorithms

DOI10.1007/S00165-012-0231-XMaRDI QIDQ1941864zbMATH OpenOpenAlexDBLPWikidataFDO

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

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)

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

Cites work

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

Cited in

(2)

• scientific article; zbMATH DE number 3976314 (Why is no real title available?)
• Structural transformations for data-enriched real-time systems

Describes a project that uses

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)