Model checking device for distributed environment model, model checking method and program for distributed environment model

摘要

When the information representing the distributed environment model is obtained, the state of the distributed environment model can be obtained by executing a plurality of linear movement moving to the second state in which the first state is the start position and the straight end position without branching at one or more transitions While searching, it is determined whether or not the searched state satisfies a predetermined property, and the sequence of transitions searched in the past and the order of transitions in each of the past linear rectilinear motions are stored in the searched stateWhen a DPOR is applied in a model checking for a distributed environment model, the search of the search after the searched state is realized, and the efficient search is carried out by storing the transition when it moves to another state in the search of the dead Made possible.