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

摘要

Upon acquiring the information indicating the distributed environment model, a plurality of linear movements are carried out in which the first state is set as a start position and the first state is linearly moved to a second state, which is an end position without branching at one or more transitions , A state that the distributed environment model can take is searched and it is judged whether or not the searched state satisfies a predetermined property and it is judged whether or not the searched state which was searched in the past and the transition in each of the linear movements executed in the past , And when DPOR is applied in model checking on a distributed environment model by storing in association with the transition at the time of moving to another state in the past search in each of the searched states, We realized the censoring of the search after the searched state and made it possible to search efficiently.