Probabilistic Verification of Communication Protocols

This procedure checks the most probable sections of the protocol behavior. Some of the ideas used in this procedure are based on a convolutional decoding procedure due to Jelinek and a performance evaluation procedure due to Rudin. A protocol is specified as a collection of FSMs interacting with one another using synchronous messages similar to those used in the programming language Communicating Sequential Processes (CSP). Multiple trees of protocol behavior are constructed.