New Approaches for Model Checking

Model checking is an algorithmic verification technique that checks automatically whether a given finite state concurrent system satisfies its temporal specification. The main disadvantage of model checking is state space explosion problem. In this paper, several important approaches have been proposed for dealing with the state explosion problem. Such approaches are symbolic, abstraction, partial.order reduction, compositional reasoning, etc. Then,a number of way are proposed for verifying real.time and hybrid systems using model checking. At last, several approaches combining model checking and other verification techniques or mathematical methods are considered.