Verification of multiprocess probabilistic protocols

DOI10.1007/BF01843570zbMath0598.68019MaRDI QIDQ1079944

Amir Pnueli, Lenore D. Zuck

Publication date: 1986

Published in: Distributed Computing (Search for Journal in Brave)

zbMATH Keywords

temporal logicdining philosophers problemextreme fairnessformal verification of probabilistic distributed programsn-processes mutual exclusion problemprobabilistic computations

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theory of operating systems (68N25)

Related Items (22)

A compositional framework for fault tolerance by specification transformation ⋮ A logic for reasoning about time and reliability ⋮ A space-efficient simulation algorithm on probabilistic automata ⋮ Model Checking Probabilistic Systems ⋮ Deriving Syntax and Axioms for Quantitative Regular Behaviours ⋮ Markov automata with multiple objectives ⋮ EVENTUAL DETERMINISM: USING PROBABILISTIC MEANS TO ACHIEVE DETERMINISTIC ENDS ⋮ Symbolic model checking for probabilistic processes ⋮ Unnamed Item ⋮ Randomized self-stabilizing and space optimal leader election under arbitrary scheduler on rings ⋮ Probabilistic verification of communication protocols ⋮ Verification of the randomized consensus algorithm of Aspnes and Herlihy: a case study ⋮ Randomized Dining Philosophers without Fairness Assumption ⋮ Generic Emptiness Check for Fun and Profit ⋮ Deciding bisimilarity and similarity for probabilistic processes. ⋮ Fair Termination for Parameterized Probabilistic Concurrent Systems ⋮ The compositional construction of Markov processes II ⋮ Symbolic Verification of Communicating Systems with Probabilistic Message Losses: Liveness and Fairness ⋮ On the verification of qualitative properties of probabilistic processes under fairness constraints. ⋮ Testing preorders for probabilistic processes can be characterized by simulations ⋮ Quantitative program logic and expected time bounds in probabilistic distributed algorithms. ⋮ Finding the closed partition of a planar graph

Cites Work

• The choice coordination problem
• Symmetric and economical solutions to the mutual exclusion problem in a distributed system
• Reasoning with time and chance
• Proving Liveness Properties of Concurrent Programs
• Termination of Probabilistic Concurrent Program
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Verification of multiprocess probabilistic protocols