An integrated algorithm for probabilistic protocol verification and evaluation

An integrated approach is presented to probabilistic verification and performance evaluation of a communication protocol. The approach, following 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⁴) to O(n²m) in generating n states and exploring m transitions. This procedure (1) is computationally very efficient; (2) 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) takes important reliability measures as its stopping criteria