2003 | OriginalPaper | Chapter
Parameterized Verification by Probabilistic Abstraction
Authors : Amir Pnueli, Lenore Zuck
Published in: Foundations of Software Science and Computation Structures
Publisher: Springer Berlin Heidelberg
Included in: Professional Book Archive
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
The paper studies automatic verification of liveness properties with probability 1 over parameterized programs that include probabilistic transitions, and proposes two novel approaches to the problem. The first approach is based on a Planner that occasionally determines the outcome of a finite sequence of “random”choices, while the other random choices are performed non-deterministically.Using a Planner, a probabilistic protocol can be treated just like a non-probabilistic one and verified as such. The second approach is based on γ-fairness, a notion of fairness that is sound and complete for verifying simple temporal properties (whose only temporal operators are ⋄and □) over finite-state systems.The paper presents a symbolic model checker based on γ-fairness.We then show how the network invariant approach can be adapted to accommodate probabilistic protocols. The utility of the Planner approach is demonstrated on a probabilistic mutual exclusion protocol. The utility of the approach of γ-fairness with network invariants is demonstrated on Lehman and Rabin's Courteous Philosophers algorithm.