MODEL INSPECTION DEVICE FOR DISTRIBUTED ENVIRONMENT MODEL, MODEL INSPECTION METHOD FOR DISTRIBUTED ENVIRONMENT MODEL, AND PROGRAM

摘要

In the present invention, when information indicating a distributed environment model is obtained, a first state is set as a starting position, and multiple linear movements are executed whereby a movement is made to a second state that is an end position by means of one or more transitions without branching, thereby retrieving states that can be assumed by the distributed environment model. A determination is made regarding whether the retrieved states satisfy a specific property, retrieved states which have been retrieved previously and the transition sequence for each of the previously executed linear movements are stored, and the transitions when moving to another state in a previous retrieval are stored in association with each of the retrieved states. Thus, when dynamic partial order reduction (DPOR) is applied in a model inspection corresponding to a distributed environment model it is possible to eliminate retrievals subsequent to a retrieved state, and thus to enable an efficient retrieval.