Probabilistic characterization of algebraic protocol specifications

A generative model for extending algebraic protocol specifications with probabilities is presented. The approach associates a simple probabilistic characterization with each algebraic operator occurrence in a behavior expression. The result is a compact notation in which the assignment of probabilities is more straightforward than with transition-based models. It is shown that an equivalent state machine with probabilities attached to transitions can be constructed automatically from an algebraic specification with probabilistic characterizations attached to operators. Specifically, it is shown how a probabilistic state machine can be derived from a basic LOTOS expression enriched by a probabilistic characterization. As an application example, a stop-and-wait protocol is examined