Probabilistic verification of Herman's self-stabilisation algorithm

DOI10.1007/S00165-012-0227-6MaRDI QIDQ1941879zbMATH OpenOpenAlexFDO

Authors Yanyan Li

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-0227-6

zbMATH Keywords

Herman's algorithmprobabilistic model checkingself-stabilisation

Mathematics Subject Classification ID

Reliability, testing and fault tolerance of networks and computer systems (68M15) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Proving the Herman-protocol conjecture
• On the expected time for Herman's probabilistic self-stabilizing algorithm
• Computing and Combinatorics
• Bounds on Herman's algorithm
• A nearly optimal upper bound for the self-stabilization time in Herman's algorithm

Cites work

• A game-based abstraction-refinement framework for Markov decision processes
• A logic for reasoning about time and reliability
• Abstraction, Refinement and Proof for Probabilistic Systems
• An elementary proof that Herman's ring is \(\Theta (N^{2})\)
• Coupling and self-stabilization
• scientific article; zbMATH DE number 3543391 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• Memory space requirements for self-stabilizing leader election protocols
• On stabilization in Herman's algorithm
• On the expected time for Herman's probabilistic self-stabilizing algorithm
• Probabilistic CEGAR
• Probabilistic self-stabilization
• Self-stabilization
• Self-stabilizing systems in spite of distributed control
• Stochastic model checking

Cited in

(15)

• Modeling and analysis of the obstacle-avoidance strategies for a mobile robot in a dynamic environment
• Inductive synthesis for probabilistic programs reaches new horizons
• Accelerating SpMV multiplication in probabilistic model checkers using GPUs
• Synthesizing optimal bias in randomized self-stabilization
• Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination
• A tighter bound for the self-stabilization time in Herman's algorithm
• Are parametric Markov chains monotonic?
• Analysis of distributed token circulation algorithm with faulty random number generator
• A nearly optimal upper bound for the self-stabilization time in Herman's algorithm
• Action and State Based Computation Tree Measurement Language and Algorithms
• Parameter synthesis for Markov models: covering the parameter space
• Using fixed memory blocks in GPUs to accelerate SpMV multiplication in probabilistic model checkers
• An oracle-guided approach to constrained policy synthesis under uncertainty
• On the expected time for Herman's probabilistic self-stabilizing algorithm
• Model checking finite-horizon Markov chains with probabilistic inference

Describes a project that uses

Uses Software

• CEGAR
• PRISM

This page was built for publication: Probabilistic verification of Herman's self-stabilisation algorithm

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