Probabilistic verification of Herman's self-stabilisation algorithm

DOI10.1007/S00165-012-0227-6zbMATH Open1259.68130OpenAlexW2030895696MaRDI QIDQ1941879FDOQ1941879

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

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

zbMATH Keywords

probabilistic model checkingHerman's algorithmself-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)

Cites Work

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

Cited In (13)

• Model checking finite-horizon Markov chains with probabilistic inference
• Parameter synthesis for Markov models: covering the parameter space
• On the expected time for Herman's probabilistic self-stabilizing algorithm
• Accelerating SpMV multiplication in probabilistic model checkers using GPUs
• A tighter bound for the self-stabilization time in Herman's algorithm
• Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination
• Action and State Based Computation Tree Measurement Language and Algorithms
• Are parametric Markov chains monotonic?
• Synthesizing optimal bias in randomized self-stabilization
• Inductive synthesis for probabilistic programs reaches new horizons
• Modeling and analysis of the obstacle-avoidance strategies for a mobile robot in a dynamic environment
• 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

Uses Software

• PRISM
• CEGAR

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)