An abstraction method developed for the explicit linear temporal logic model checking was geared towards reducing the useless part of the state space during the abstraction period. This reduces the cost during the abs...An abstraction method developed for the explicit linear temporal logic model checking was geared towards reducing the useless part of the state space during the abstraction period. This reduces the cost during the abstraction period relative to models requiring many useless states. A dining-philosophers example comparing this abstraction method with conventional methods indicates that a large proportion of the state space has been reduced by this abstraction method. Finally, the abstract method is shown to be correct and an analysis is given to show how such a large proportion of states can be reduced.展开更多
基金Supported by the National Natural Science Foundation of China(No. 60635020)the Basic Research Foundation of Tsinghua National Laboratory for Information Science and Technology(TNList)
文摘An abstraction method developed for the explicit linear temporal logic model checking was geared towards reducing the useless part of the state space during the abstraction period. This reduces the cost during the abstraction period relative to models requiring many useless states. A dining-philosophers example comparing this abstraction method with conventional methods indicates that a large proportion of the state space has been reduced by this abstraction method. Finally, the abstract method is shown to be correct and an analysis is given to show how such a large proportion of states can be reduced.
