Global state graph reduction techniques for protocol validation in the EFSM model

In the EFSM (extended finite state machine) model, the behavior of each protocol entity is described as a finite state machine (FSM), and a set of context variables declared for the entity can be accessed during state transitions. One of the most severe difficulties in using reachability analysis for protocol validation in the EFSM model is the global state explosion problem. The problem is caused in part by a wide range of possible values that could be taken on by a context variable. To alleviate the effect of context variables on the global state explosion problem, two global state graph reduction techniques are proposed. In the first reduction technique, the authors define a global state equivalence based on dead variable sets. The global state graph is then generated taking the global state equivalence into consideration. An upper bound for the effect of the first reduction technique on the reduction of the global state graph is shown. A second reduction technique based on a similar reasoning is derived to complement the first reduction technique.<>