Verification of multiprocess probabilistic protocols
From MaRDI portal
In this paper we demonstrate the utility of temporal logic to the formal verification of probabilistic distributed programs. The approach taken is to represent the quantitative notion of probabilistic computations by the qualitative abstraction of extreme fairness. The method is illustrated first on the dining philosophers problem and then on a new probabilistic symmetric solution to the n-processes mutual exclusion problem. Two related solutions are presented corresponding to different assumptions about the granularity of a compound test.
Recommendations
- Probabilistic verification of communication protocols
- A Proof System for Compositional Verification of Probabilistic Concurrent Processes
- FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
- Verification of Probabilistic Programs
- Verification of probabilistic systems with faulty communication
- scientific article; zbMATH DE number 1956504
- Parameterized verification of many identical probabilistic timed processes
- On verification of parallel message-passing processes
- Message-passing algorithms for the verification of distributed protocols
Cites work
- scientific article; zbMATH DE number 3829244 (Why is no real title available?)
- scientific article; zbMATH DE number 3940713 (Why is no real title available?)
- scientific article; zbMATH DE number 3755842 (Why is no real title available?)
- scientific article; zbMATH DE number 3800906 (Why is no real title available?)
- Proving Liveness Properties of Concurrent Programs
- Reasoning with time and chance
- Symmetric and economical solutions to the mutual exclusion problem in a distributed system
- Termination of Probabilistic Concurrent Program
- The choice coordination problem
Cited in
(31)- Finding the closed partition of a planar graph
- A compositional framework for fault tolerance by specification transformation
- A logic for reasoning about time and reliability
- Testing preorders for probabilistic processes can be characterized by simulations
- Quantitative program logic and expected time bounds in probabilistic distributed algorithms.
- Probabilistic verification
- A temporal logic for proving properties of topologically general executions
- Randomized self-stabilizing and space optimal leader election under arbitrary scheduler on rings
- Deciding bisimilarity and similarity for probabilistic processes.
- Modular verification of protocol equivalence in the presence of randomness
- On the verification of qualitative properties of probabilistic processes under fairness constraints.
- A space-efficient simulation algorithm on probabilistic automata
- The compositional construction of Markov processes. II
- Model checking probabilistic systems
- Deriving Syntax and Axioms for Quantitative Regular Behaviours
- Generic emptiness check for fun and profit
- Fair termination for parameterized probabilistic concurrent systems
- Symbolic Verification of Communicating Systems with Probabilistic Message Losses: Liveness and Fairness
- scientific article; zbMATH DE number 4080970 (Why is no real title available?)
- scientific article; zbMATH DE number 1956507 (Why is no real title available?)
- Symbolic model checking for probabilistic processes
- Logic-based verification of the distributed dining philosophers protocol
- scientific article; zbMATH DE number 2087627 (Why is no real title available?)
- EVENTUAL DETERMINISM: USING PROBABILISTIC MEANS TO ACHIEVE DETERMINISTIC ENDS
- A Proof System for Compositional Verification of Probabilistic Concurrent Processes
- Verification of the randomized consensus algorithm of Aspnes and Herlihy: a case study
- Randomized dining philosophers without fairness assumption
- Using Probabilistic Kleene Algebra for Protocol Verification
- Verification of randomized consensus algorithms under round-rigid adversaries
- Compositional verification of randomized distributed algorithms
- Probabilistic verification of communication protocols
This page was built for publication: Verification of multiprocess probabilistic protocols
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1079944)
