As computer hardware and software systems become more and more complex

how to assure the correctness and reliability of such system sbecomes an urgent problem. Among theories proposed as solutions to this problem

model checking has become a very attractive and appealing approach

because of its simplicity and high level of automation. Research on model checking covers the following subjects: modal/temporal logics

model checking algorithms

efficiency of model checking with respect to time and space(especially space complexity)

and development of model checking tools. These aspects are closely related. Complexities of model checking algorithms vary very much for different modal/temporal logics

and optimizations are often targeted at certain types of logic fonnulas. Some new achievements and research directions are also discussed.