Protocol Validation by Maximal Progress State Exploration

We discuss an efficient variation of state exploration for two communicating finite state machines. In particular, we propose to divide the task of generating all reachable states into two independent subtasks. In each subtask, only the states reachable by forcing maximal progress for one machine are generated. Since the two subtasks are completely independent, and since in most instances the time and storage requirements for each subtask are less than those for the original task, maximal Progress state exploration can save time and/or storage over conventional state exploration.