2003 | OriginalPaper | Buchkapitel
Parameterized Verification by Probabilistic Abstraction
verfasst von : Amir Pnueli, Lenore Zuck
Erschienen in: Foundations of Software Science and Computation Structures
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. 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.