An integrated algorithm for probabilistic protocol verification and evaluation

This paper presents an integrated approach to probabilistic verification and performance evaluation of a communication protocol. The approach, following the Best-First rules, generates, verifies, and evaluates states and transitions in a global reachability graph. A new recursion is found to reduce the computational complexity of the procedure from O(n 4) to O(n 2m) in generating n states and exploring m transitions. This procedure is unique in that (1) it is computationally very efficient and (2) it provides interesting performance and reliability measures such as Mean Time To Unknown, which is the average operation time before any unchecked scenario occurs, and protocol throughput, and (3) it takes important reliability measures as its stopping criteria. © 1989 IEEE.