Reasoning About Probabilistic Behavior in Concurrent Systems
- 1 June 1987
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Software Engineering
- Vol. SE-13 (6) , 740-745
- https://doi.org/10.1109/tse.1987.233478
Abstract
Certain aspects of the behavior of concurrent systems are intrinsically probabilistic in nature, e.g., the behavior of imperfect communication media used in network protocols. We address the problem of expressing such behavior in an algebraic calculus for communicating systems. The introduction of probabilistic information in the calculus alleviates the problem of proving liveness, as proving liveness now amounts to proving that its probability is 1. A methodology for proving both safety and liveness is developed and used in proving the correctness of the Alternating Bit Protocol.Keywords
This publication has 0 references indexed in Scilit: