STATIC PARTIAL ORDER REDUCTION

摘要

A static partial order reduction generator and process result in a substantially reduced state space graph of a multi-process system, independently of the model checking process. The process of this invention creates a modified state graph generator with appended rules that allow any desired state searching tactic (bre adth first, depth first, etc.) to be employed when states and transitions are conside red in the course of verification. This permits use of existing model checking tools without needing to modify them. The static partial order reduction is made possi ble by realizing that a prior art condition that at least one state along each cycle of the reduced state graph must be fully expanded can be guaranteed by considering the individual processes that make up the system and identifying certain transitions in those processes.