Abstract: Lazy slicing is an effective state-space reduction method, but it can not directly determine whether a model satisfies the expected linear property. A lazy slicing based method is proposed to solve this problem. First, it constructs a negation Büchi automaton for given linear temporal logic formula and a product automaton of the system model. Then it searches for an acceptable trace on this product automaton lazily. Thus, the problem of verifying a linear time property is converted into the problem of invariance validation, which makes it possible to search the acceptable state by reachability analysis. Experiment results show that this lazy slicing based algorithm not only makes lazy slicing be able to verify linear time property, but also remarkably improves the scalability of LTL model checking.